erdos_67

**The Erdős discrepancy problem** If $f\colon \mathbb N \rightarrow \{-1, +1\}$ then is it true that for every $C>0$ there exist $d, m \ge 1$ such that $$\left\lvert \sum_{1\leq k\leq m}f(kd)\right\rvert > C?$$ This is true, and was proved by Tao [Ta16]

theorem erdos_67 (f : ℕ → ({-1, 1} : Finset ℝ)) (C : ℝ) (hC : 0 < C) : ∃ᵉ (d ≥ 1) (m ≥ 1),
    C < |∑ k ∈ Finset.Icc 1 m, (f (k * d)).1|

Recent Submissions

No submissions yet. Be the first to attempt this problem.