Erdős problem 498
Let with for . Let be an arbitrary disc of radius . Is it true that the number of sums of the shape which lie in is at most ?
Sources
FormalConjectures/ErdosProblems/
498.lean
Retained formal statement
Let with for . Let be an arbitrary disc of radius . Is it true that the number of sums of the shape which lie in is at most ?
A strong form of the Littlewood-Offord problem. Erdős [Er45] proved this is true if , and for general proved a weaker upper bound of This was solved in the affirmative by Kleitman [Kl65], who also later generalised this to arbitrary Hilbert spaces [Kl70].
See also [395].
True ↔ ∀ (n : ℕ) (z : Fin n → ℂ), (∀ (i : Fin n), 1 ≤ ‖z i‖) → ∀ (c : ℂ), {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z i ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)SolvedStatement only, no proof