Erdős problem 510 · problems.science

Chowla's cosine problem

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

510.lean

Retained formal statement3 of 3

Ruzsa [Ru04] proved an upper bound of $-\exp(O(\sqrt{\log N})$ .

FormalConjectures/ErdosProblems/510.leanErdos510.erdos_510.variants.ruzsa4 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 * θ) < -Real.exp (c * √(Real.log ↑N))

SolvedStatement only, no proof

Sources

Search problems.science