Skip to content

Erdős problem 67

Start work

The Erdős discrepancy problem

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

67.lean

Retained formal statement1 of 2

The Erdős discrepancy problem

If f ⁣:N→{−1,+1}f\colon \mathbb N \rightarrow \{-1, +1\} then is it true that for every C>0C>0 there exist d,m≥1d, m \ge 1 such that ∣∑1≤k≤mf(kd)∣>C?\left\lvert \sum_{1\leq k\leq m}f(kd)\right\rvert > C? This is true, and was proved by Tao [Ta16]

FormalConjectures/ErdosProblems/67.leanErdos67.erdos_671 lineExact file
∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|
SolvedStatement only, no proof