Littlewood–Offord problem

TheoremSharp Littlewood–Offord bound#●ready to prove

There is a real constant \(A \ge 0\) such that for every integer \(n \ge 1\) and all real numbers \(a_0, a_1, \dots, a_n\) with \(|a_i| \ge 1\) for every \(i\), the number of sign vectors \((\varepsilon_1, \dots, \varepsilon_n) \in \{-1, 1\}^n\) with \(|a_0 + \varepsilon_1 a_1 + \dots + \varepsilon_n a_n| < 1\) is at most \(A \cdot 2^n / \sqrt{n}\).

This answers Offord's Problem 179 from the Scottish Book. In the original notation the bound is on the exceptional set of signed sums \(a_0 + \varepsilon_1 a_1 + \dots + \varepsilon_n a_n\) whose absolute value is below \(\min_\nu |a_\nu|\); the statement here is the rescaled form with \(\min_\nu |a_\nu| = 1\).

theorem_wanted littlewoodOffordSharpBound :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (a : Fin (n + 1) → ℝ),
      (∀ i, 1 ≤ |a i|) →
      ((Finset.univ.filter (fun ε : Fin n → Bool =>
        |a 0 + ∑ i : Fin n, (if ε i then (1 : ℝ) else -1) * a (Fin.succ i)| < 1)).card :
        ℝ) ≤ A * (2 : ℝ) ^ n / Real.sqrt n

Sources

A. C. Offord, Problem 179 of the Scottish Book; the Littlewood-Offord lemma (Littlewood-Offord, 1938) and Erdős's proof giving the sharp O(2 ^ n / √n) bound, attained when all the a nu are equal. See the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

DefinitionStrong Littlewood–Offord bound in the plane#✓fully proved

The statement that for every natural number \(n\), all complex numbers \(z_1, \dots, z_n\) with \(|z_i| \ge 1\) for every \(i\), and every open disc \(D\) of radius \(1\) in \(\mathbb{C}\), at most \(\binom{n}{\lfloor n/2 \rfloor}\) of the \(2^n\) sign vectors \((\varepsilon_1, \dots, \varepsilon_n) \in \{1, -1\}^n\) satisfy \(\sum_i \varepsilon_i z_i \in D\) (Erdős Problem 498).

def signedSumsInUnitDiscBound : Prop :=
  ∀ (n : ℕ) (z : Fin n → ℂ), (∀ i, 1 ≤ ‖z i‖) → ∀ c : ℂ,
    {ε : Fin n → Bool | ∑ i, (if ε i then (1 : ℂ) else -1) * z i ∈ Metric.ball c 1}.ncard ≤
      n.choose (n / 2)

Used by 1

Used byKleitman's theorem on signed sums in the plane

TheoremKleitman's theorem on signed sums in the plane#●ready to prove

For every natural number \(n\), all complex numbers \(z_1, \dots, z_n\) with \(|z_i| \ge 1\) for every \(i\), and every open disc \(D\) of radius \(1\) in \(\mathbb{C}\), at most \(\binom{n}{\lfloor n/2 \rfloor}\) of the \(2^n\) sign vectors \((\varepsilon_1, \dots, \varepsilon_n) \in \{1, -1\}^n\) satisfy \(\sum_i \varepsilon_i z_i \in D\).

Kleitman proved this bound for complex \(z_i\) (later for vectors in any Hilbert space); Erdős had proved it for real \(z_i\).

public theorem_wanted signedSumsInUnitDiscBound_holds : signedSumsInUnitDiscBound

def signedSumsInUnitDiscBound : Prop :=
  ∀ (n : ℕ) (z : Fin n → ℂ), (∀ i, 1 ≤ ‖z i‖) → ∀ c : ℂ,
    {ε : Fin n → Bool | ∑ i, (if ε i then (1 : ℂ) else -1) * z i ∈ Metric.ball c 1}.ncard ≤
      n.choose (n / 2)

WantedExt/Combinatorics/StrongLittlewoodOffordErdosProblem498Wanted.lean:37

Sources

T. F. Bloom, Erdős Problems, Problem #498, https://www.erdosproblems.com/498 (status PROVED (LEAN)); resolution: D. J. Kleitman, On a lemma of Littlewood and Offord on the distribution of certain sums, Math. Z. (1965), 251-259, erdosproblems.com/498: solved in the affirmative by Kleitman; generalized to Hilbert spaces (Kleitman 1970), https://www.erdosproblems.com/498.

Uses 1

Statement usesStrong Littlewood–Offord bound in the plane

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.