erdős #67 · Erdős discrepancy problem
If then is it true that for every there exist such that
Worked, still open.
discrepancy · solved · prize $500 · formalized (Lean) · 0 attempts
machinery: multiplicative-functions,discrepancy,Elliott-conjecture,additive-combinatorics,prime-distribution
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · solved (literature)
theorem erdos_67 (f : ℕ → ({-1, 1} : Finset ℝ)) (C : ℝ) (hC : 0 < C) : ∃ᵉ (d ≥ 1) (m ≥ 1),
C < |∑ k ∈ Finset.Icc 1 m, (f (k * d)).1|formal-conjectures/67.lean ↗oeis
A181740 — Number of sequences of length n over {1, -1} with Erdős discrepancy <= 2.1,2,4,6,12,18,28,44,88,100,152,240,370,556,882,750,1500,2250,2784,4284,6438,6062,9526,14856,22944,26164,39528,35122,5480A237695 — Maximum length of a +- 1 sequence of discrepancy n.0,11,1160
links
proved · paper
status
solved