Erdős problem 67
The Erdős discrepancy problem
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/67.lean∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|SolvedStatement only, no proof