Erdős discrepancy problem
Closed
Theorem & proof
·
erdos_discrepancy.lean
·
✓ verified
1
2
3
import Mathlib theorem erdos_discrepancy : ∀ (s : ℕ → ({-1, 1} : Set ℤ)), ∀ C : ℝ, ∃ d n : ℕ, 0 < d ∧ 0 < n ∧ C < |∑ k ∈ Finset.range n, (s (d * (k + 1)) : ℝ)| :=sorry
Rewards pledged
No rewards pledged yet.