Problem

erdos:510

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

Open Current State

Declared status: open
Formalization: formalized
Subjects: analysis
OEIS: N/A
Sources: source:erdos-problemssource:formal-conjectures
Statement: www.erdosproblems.com

Chowla's cosine problem

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims