Erdős Problem 67

References:

• erdosproblems.com/67
• [Ta16] Tao, Terence, The Erdős discrepancy problem. Discrete Anal. (2016), Paper No. 1, 29.

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

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 Erdos67.erdos_67.variants.complex (f : ℕ → ↑(Metric.sphere 0 1)) (C : ℝ) (hC : 0 < C) : ∃ d ≥ 1, ∃ m ≥ 1, C < ‖∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))‖

The Erdős discrepancy problem (complex variant)

If $f\colon \mathbb N \rightarrow S^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]