Erdős problem 510

Chowla's cosine problem

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

510.lean

Retained formal statement2 of 3

Bedert [Be25c] proved an upper bound of $-c N^{1/7}$ .

FormalConjectures/ErdosProblems/510.leanErdos510.erdos_510.variants.bedert4 linesExact file

1∃ c,2  ∃ (_ : 0 < c),3    ∀ᶠ (N : ℕ) in Filter.atTop,4      ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ θ, ∑ n ∈ A, Real.cos (↑n * θ) < -c * ↑N ^ (1 / 7)

SolvedStatement only, no proof