Skip to content

Erdős problem 510

Chowla's cosine problem

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/510.lean

Formal Conjectures

FormalConjectures/ErdosProblems/510.leanErdos510.erdos_5104 linesExact file
sorryc,    ∃ (_ : 0 < c),      ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ AA.card = N → ∃ θ, ∑ nA, Real.cos (↑n * θ) < -c * √↑N
OpenStatement only, no proof

Continue

Search problems.science

Find a Problem, Result, source, or page