feat: add Green's Open Problem 82

[krrish175-byte]

Closes #1737

This PR formalizes Green's Open Problem 82, which asks: for a finite set A ⊂ ℤ of size n, what is the minimum number of zeros that ∑_{a∈A} cos(2πaθ) must have on ℝ/ℤ?

[felixpernegger]

n probably shouldnt be in the context as usual

[felixpernegger]

Better write this as an inequality and not take sup?

[felixpernegger]

The green problem list mentions known bounds, please include them.

[felixpernegger]

This is not what the problem is asking. Why do you have to limit $\theta$ to Ico 0 1?

[krrish175-byte]

Thanks for the review. Sorry, I missed those. I have updated the code as you asked for:

• Moved n inside the theorem statement.
• Reformulated the statement using an inequality.
• Added the known lower bound $\Omega(\log n / \log \log n)$.

Regarding Ico 0 1: Since the trigonometric polynomial is 1-periodic, counting zeros in the fundamental domain [0, 1) seemed like the most direct way to represent the count on R / Z. Let me know if you would prefer using UnitAddCircle instead. Thanks for the review again!

[felixpernegger]

Thanks for the review. Sorry, I missed those. I have updated the code as you asked for:

* Moved n inside the theorem statement.

* Reformulated the statement using an inequality.

* Added the known lower bound 
    Ω
    (
    log
    ⁡
    n
    
      /
    
    log
    ⁡
    log
    ⁡
    n
    )
  .

Regarding Ico 0 1: Since the trigonometric polynomial is 1-periodic, counting zeros in the fundamental domain [0, 1) seemed like the most direct way to represent the count on R / Z. Let me know if you would prefer using UnitAddCircle instead. Thanks for the review again!

Thank you ChatGPT. I mistook what R / Z meant in this context, yeah.

[felixpernegger]

Where did you get this estimate from? Its not mentioned on the website....
If you include known results, also make sure to reference them properly.

In theory, it is fine if you use AI assistance (sorry if im mistaken, but im pretty sure), but it is crucial you check the output.

On a nother note, there are also bounds in the other direction as mentioned in the problem list, which should be included as well.

[krrish175-byte]

I really really apologize for the confusion.

I went back to the original problem statement in Green's paper and I see now that I misread/misunderstood the bounds mentioned. The paper doesn't actually specify concrete bounds for Problem 82, so I shouldn't have included that theorem. I accept its my mistake.

Regarding the Ico 0 1 restriction, you make a good point. I was thinking about the periodicity, but the problem is really asking about the minimum number of zeros as we vary over all possible finite sets A, which is indeed a different question than counting in a fundamental domain.

I will update the PR to remove that lower bound theorem entirely, reformulate without the [0,1) restriction, keep it as an inequality as you suggested

Thanks again for the review, this is my first contribution to this project and I'm still learning the conventions so I request your patience and assistance. Thanks again...

[felixpernegger]

The Ico thing should be fine though.

[krrish175-byte]

Ah got it. Thanks for clarifying. Then I will keep the Ico 0 1 restriction then. So before I push any changes, can you please confirm if this approach is right or you need any more changes :

1. Ico 0 1 kept (as you just confirmed)
2. The incorrect lower bound removed
3. n ≥ 2 instead of n ≥ 1
4. The upper bound n^{5/6} included

let me know if there's anything else that needs adjustment

[felixpernegger]

According to the problem list, n^ 5/6 isnt the best known bound anymore.

I dont know why you need 1 leq n or 2 leq n. Everything is in Landau O notation, so this shouldnt matter.

There are known results both on the upper and lower bound. A complete foramilasation ought to nention both of them.

[felixpernegger]

According to the problem list, n^ 5/6 isnt the best known bound anymore.

I dont know why you need 1 leq n or 2 leq n. Everything is in Landau O notation, so this shouldnt matter.

There are known results both on the upper and lower bound. A complete foramilasation ought to nention both of them.

[krrish175-byte]

I have updated the code with the current best known bounds:

Lower bound: (log log n)^c for sufficiently large n

• wReference: Bedert (2025), arXiv:2407.16075

Upper bound: C(n log n)^(2/3)

• Reference: Juškevičius & Sahasrabudhe (2020), arXiv:2005.01695

I've formalized both bounds as separate theorems as you suggested. The lower bound uses ∃ n0 to handle the asymptotic nature properly (since log log n isn't well-defined for small n).

Let me know if it is correct now.