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 statement1 of 3

Chowla's cosine problem

If $A\subset \mathbb{N}$ is a finite set of positive integers of size $N > 0$ then is there some absolute constant $c>0$ and $\theta$ such that $\sum_{n\in A}\cos(n\theta) < -cN^{1/2}?$

FormalConjectures/ErdosProblems/510.leanErdos510.erdos_5104 linesExact file

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

OpenStatement only, no proof

Sources

Search problems.science