Skip to content

Erdős problem 498

Let z1,…,zn∈Cz_1,\ldots,z_n\in\mathbb{C} with 1≤∣zi∣1\leq \lvert z_i\rvert for 1≤i≤n1\leq i\leq n. Let DD be an arbitrary disc of radius 11. Is it true that the number of sums of the shape ∑i=1nϵizi for ϵi∈{−1,1}\sum_{i=1}^n\epsilon_iz_i \textrm{ for }\epsilon_i\in \{-1,1\} which lie in DD is at most (n⌊n/2⌋)\binom{n}{\lfloor n/2\rfloor}?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

498.lean

Retained formal statement1 of 1

Let z1,…,zn∈Cz_1,\ldots,z_n\in\mathbb{C} with 1≤∣zi∣1\leq \lvert z_i\rvert for 1≤i≤n1\leq i\leq n. Let DD be an arbitrary disc of radius 11. Is it true that the number of sums of the shape ∑i=1nϵizi for ϵi∈{−1,1}\sum_{i=1}^n\epsilon_iz_i \textrm{ for }\epsilon_i\in \{-1,1\} which lie in DD is at most (n⌊n/2⌋)\binom{n}{\lfloor n/2\rfloor}?

A strong form of the Littlewood-Offord problem. Erdős [Er45] proved this is true if zi∈Rz_i\in\mathbb{R}, and for general zi∈Cz_i\in\mathbb{C} proved a weaker upper bound of ≪2nn.\ll \frac{2^n}{\sqrt{n}}. This was solved in the affirmative by Kleitman [Kl65], who also later generalised this to arbitrary Hilbert spaces [Kl70].

See also [395].

FormalConjectures/ErdosProblems/498.leanErdos498.erdos_4985 linesExact file
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