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

The Erdős discrepancy problem (complex variant)

If f ⁣:N→S1⊆Cf\colon \mathbb N \rightarrow S^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_67.variants.complex1 lineExact file
∀ (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