Skip to content

Erdős problem 510

Start work

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
sorry ↔  ∃ c,    ∃ (_ : 0 < c),      ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ θ, ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N
OpenStatement only, no proof

Continue

Start a contributionBrowse the source filesOpen the collection entry