Erdős problem 67 · problems.science

The Erdős discrepancy problem

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

67.lean

Retained formal statement1 of 2

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]

FormalConjectures/ErdosProblems/67.leanErdos67.erdos_671 lineExact file

1∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|

SolvedStatement only, no proof

Sources

Search problems.science