/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilBen Green's Open Problem 82
References:
An improved lower bound for a problem of Littlewood on the zeros of cosine polynomials (Bedert, 2025)
Cosine polynomials with few zeros (Juškevičius & Sahasrabudhe, 2020)
open Filter Real Setopen scoped Finsetnamespace Green82The minimum number of zeros in $[0,1)$ of $\sum_{a \in A} \cos(2\pi a\theta)$ over all sets $A \subset \mathbb{Z}$ of size $n$.
noncomputable def minZeros (n : ℕ+) : ℕ∞ :=
⨅ A : {A : Finset ℤ // A.card = n},
({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A.val, cos (2 * π * a * θ) = 0} : Set ℝ).ncard
Let $A \subset \mathbb{Z}$ be a set of size $n$. For how many $\theta \in \mathbb{R}/\mathbb{Z}$
must we have $\sum_{a \in A} \cos(2\pi a\theta) = 0$? The answer is the function minZeros.
@[category research open, AMS 11 42]
theorem green_82 : (answer(sorry) : ℕ+ → ℕ∞) = minZeros := ⊢ sorry = minZeros
All goals completed! 🐙Lower bound: every set has at least $(\log \log n)^{1-o(1)}$ zeros.
@[category research solved, AMS 11 42]
theorem green_82_lower_bound :
∃ o : ℕ → ℝ, o =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
∀ᶠ n in atTop, ∀ A : Finset ℤ, A.card = n →
(⌊(Real.log (Real.log n)) ^ (1 - |o n|)⌋₊ : ℕ∞) ≤
({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * a * θ) = 0} : Set ℝ).ncard := ⊢ ∃ o,
(o =o[atTop] fun x ↦ 1) ∧
∀ᶠ (n : ℕ) in atTop,
∀ (A : Finset ℤ),
#A = n → ↑⌊log (log ↑n) ^ (1 - |o n|)⌋₊ ≤ ↑{θ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * ↑a * θ) = 0}.ncard
All goals completed! 🐙Upper bound: there exists $A$ with at most $C(n \log n)^{2/3}$ zeros.
@[category research solved, AMS 11 42]
theorem green_82_upper_bound :
∃ C > 0, ∀ n ≥ 1, ∃ A : Finset ℤ, A.card = n ∧
({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * a * θ) = 0} : Set ℝ).ncard ≤
(⌊C * (n * Real.log n) ^ (2 / 3 : ℝ)⌋₊ : ℕ∞) := ⊢ ∃ C > 0,
∀ n ≥ 1, ∃ A, #A = n ∧ ↑{θ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * ↑a * θ) = 0}.ncard ≤ ↑⌊C * (↑n * log ↑n) ^ (2 / 3)⌋₊
All goals completed! 🐙end Green82