Tomaszewski's conjecture
DefinitionTomaszewski's conjecture#✓fully proved
The statement that for every natural number \(n\) and every vector \(a = (a_1, \dots, a_n) \in \mathbb{R}^n\) with \(a_1^2 + \dots + a_n^2 = 1\), at least half of the \(2^n\) sign vectors \(x \in \{-1, 1\}^n\) satisfy \(|a_1 x_1 + \dots + a_n x_n| \le 1\).
def tomaszewskiConjecture : Prop :=
∀ (n : ℕ) (a : Fin n → ℝ), ∑ i, a i ^ 2 = 1 →
(2 : ℝ) ^ n ≤ 2 * ((Finset.univ.filter fun x : Fin n → Bool =>
|∑ i, a i * (if x i then (1 : ℝ) else -1)| ≤ 1).card : ℝ)Sources
- O'Donnell, Open Problems in Analysis of Boolean Functions, Problem 2. A sign vector is a map
x : Fin n → Bool, withtrueread as1andfalseas-1.
Used by 1
TheoremTomaszewski's conjecture holds#●ready to prove
For every natural number \(n\) and every vector \(a = (a_1, \dots, a_n) \in \mathbb{R}^n\) with \(a_1^2 + \dots + a_n^2 = 1\), at least half of the \(2^n\) sign vectors \(x \in \{-1, 1\}^n\) satisfy \(|a_1 x_1 + \dots + a_n x_n| \le 1\); equivalently, for a uniformly random sign vector \(x\) this inequality holds with probability at least \(1/2\).
public theorem_wanted tomaszewskiConjecture_holds : tomaszewskiConjecturedef tomaszewskiConjecture : Prop :=
∀ (n : ℕ) (a : Fin n → ℝ), ∑ i, a i ^ 2 = 1 →
(2 : ℝ) ^ n ≤ 2 * ((Finset.univ.filter fun x : Fin n → Bool =>
|∑ i, a i * (if x i then (1 : ℝ) else -1)| ≤ 1).card : ℝ)WantedExt/Combinatorics/TomaszewskiRandomSignedSumAMR127Problem0002Wanted.lean:41
Sources
- R. O'Donnell, Open Problems in Analysis of Boolean Functions (2012), arXiv:1204.6447, Problem 2 (Tomaszewski's Conjecture); resolution: N. Keller and O. Klein, Proof of Tomaszewski's conjecture on randomly signed sums, Adv. Math. 407 (2022), 108558, arXiv:2006.16834, main theorem (Section 1): for X = ∑ aᵢxᵢ with ∑ aᵢ² = 1 and independent uniform xᵢ ∈ {-1, 1}, Pr[|X| ≤ 1] ≥ 1/2, https://arxiv.org/abs/2006.16834.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.