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 statement2 of 2

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]

FormalConjectures/ErdosProblems/67.leanErdos67.erdos_67.variants.complex1 lineExact file

1∀ (f : ℕ → ↑(Metric.sphere 0 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