Cauchy–Schwarz and the choice of weights

The lemma that removes the weights (Lemma 5.3 of the paper, Section 5.2), for two finite families of non-negative vectors (no cube). The steps of its proof: the Cauchy–Schwarz inequality over the pairs (Step 1, pair_cs), the choice of the weights w j = 1 / (√(X j * Y j) + ε) with ε → 0 (Step 2, weight_choice), the Cauchy–Schwarz inequality over the coordinates (Step 3, in cs_core), and the conclusion (le_of_sq_le_mul).

abstract_cs (Lemma 5.3): if the sums ∑_{j ∈ D x y} w j * a x j * b y j are positive and ∑_{x ∈ O} ∑_{y ∈ N} (∑_{j ∈ D x y} w j * a x j * b y j)⁻¹ ≤ C * ∑ j, (w j)⁻¹ for every positive weight vector w, then (∑_{x ∈ O} (∑ j, a x j)⁻¹) * (∑_{y ∈ N} (∑ j, b y j)⁻¹) ≤ C.

The lemma abstract_cs is used twice: for the two-sided inequality (RemoveWeights.lean) and for the third-moment inequality (Level/ThirdMoment.lean).

theorem AaronsonAmbainis.inv_sq_mul_self (s : ℝ) : s⁻¹ ^ 2 * s = s⁻¹

s⁻¹ ^ 2 * s = s⁻¹ for every real s (also for s = 0).

theorem AaronsonAmbainis.sum_mul_rows {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] (O : Finset α) (N : Finset β) (w : ι → ℝ) (u : α → ℝ) (v : β → ℝ) (f : α → ι → ℝ) (h : β → ι → ℝ) : ∑ j : ι, (w j * ∑ x ∈ O, u x * f x j) * ∑ y ∈ N, v y * h y j = ∑ x ∈ O, ∑ y ∈ N, u x * v y * ∑ j : ι, w j * f x j * h y j

Expanding a weighted sum of products of two combinations of rows.

theorem AaronsonAmbainis.pair_cs {α : Type u_1} {β : Type u_2} (O : Finset α) (N : Finset β) (c s : α → β → ℝ) (hs : ∀ x ∈ O, ∀ y ∈ N, 0 < s x y) : (∑ x ∈ O, ∑ y ∈ N, c x y) ^ 2 ≤ (∑ x ∈ O, ∑ y ∈ N, c x y ^ 2 * s x y) * ∑ x ∈ O, ∑ y ∈ N, (s x y)⁻¹

Cauchy–Schwarz over pairs.

theorem AaronsonAmbainis.le_of_forall_eps {Q S C c : ℝ} (hS : 0 ≤ S) (hC : 0 ≤ C) (hc : 0 ≤ c) (h : ∀ (ε : ℝ), 0 < ε → Q ≤ S * (C * (S + c * ε))) : Q ≤ C * S ^ 2

If Q ≤ S * (C * (S + c * ε)) for every ε > 0, then Q ≤ C * S ^ 2.

theorem AaronsonAmbainis.weight_choice {ι : Type u_1} [Fintype ι] (X Y : ι → ℝ) (hX : ∀ (j : ι), 0 ≤ X j) (hY : ∀ (j : ι), 0 ≤ Y j) (C Q : ℝ) (hC : 0 ≤ C) (h : ∀ (w : ι → ℝ), (∀ (j : ι), 0 < w j) → Q ≤ (∑ j : ι, w j * X j * Y j) * (C * ∑ j : ι, (w j)⁻¹)) : Q ≤ C * (∑ j : ι, √(X j * Y j)) ^ 2

The choice of the weights w j = 1 / (√(X j * Y j) + ε), ε → 0 (Step 2 of the proof of Lemma 5.3 of the paper).

theorem AaronsonAmbainis.le_of_sq_le_mul {P C : ℝ} (hC : 0 ≤ C) (h : P ^ 2 ≤ C * P) : P ≤ C

P ^ 2 ≤ C * P and 0 ≤ C give P ≤ C.

theorem AaronsonAmbainis.cs_core {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] (O : Finset α) (N : Finset β) (a : α → ι → ℝ) (b : β → ι → ℝ) (ha : ∀ (x : α) (j : ι), 0 ≤ a x j) (hb : ∀ (y : β) (j : ι), 0 ≤ b y j) (u : α → ℝ) (v : β → ℝ) (hua : ∀ (x : α), u x ^ 2 * ∑ j : ι, a x j = u x) (hvb : ∀ (y : β), v y ^ 2 * ∑ j : ι, b y j = v y) (D : α → β → Finset ι) (C : ℝ) (hC : 0 ≤ C) (hpos : ∀ x ∈ O, ∀ y ∈ N, ∀ (w : ι → ℝ), (∀ (j : ι), 0 < w j) → 0 < ∑ j ∈ D x y, w j * a x j * b y j) (hpairs : ∀ (w : ι → ℝ), (∀ (j : ι), 0 < w j) → ∑ x ∈ O, ∑ y ∈ N, (∑ j ∈ D x y, w j * a x j * b y j)⁻¹ ≤ C * ∑ j : ι, (w j)⁻¹) : (∑ x ∈ O, u x) * ∑ y ∈ N, v y ≤ C

The Cauchy–Schwarz argument with general coefficients u, v satisfying u x ^ 2 * ∑ j, a x j = u x and v y ^ 2 * ∑ j, b y j = v y.

theorem AaronsonAmbainis.abstract_cs {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] (O : Finset α) (N : Finset β) (a : α → ι → ℝ) (b : β → ι → ℝ) (ha : ∀ (x : α) (j : ι), 0 ≤ a x j) (hb : ∀ (y : β) (j : ι), 0 ≤ b y j) (D : α → β → Finset ι) (C : ℝ) (hC : 0 ≤ C) (hpos : ∀ x ∈ O, ∀ y ∈ N, ∀ (w : ι → ℝ), (∀ (j : ι), 0 < w j) → 0 < ∑ j ∈ D x y, w j * a x j * b y j) (hpairs : ∀ (w : ι → ℝ), (∀ (j : ι), 0 < w j) → ∑ x ∈ O, ∑ y ∈ N, (∑ j ∈ D x y, w j * a x j * b y j)⁻¹ ≤ C * ∑ j : ι, (w j)⁻¹) : (∑ x ∈ O, (∑ j : ι, a x j)⁻¹) * ∑ y ∈ N, (∑ j : ι, b y j)⁻¹ ≤ C

The lemma that removes the weights (Lemma 5.3 of the paper): Steps 1–3 and the conclusion of its proof. The reciprocals are ⁻¹, with 0⁻¹ = 0 in Lean, and the sets O and N may be empty; so the first assertion of Lemma 5.3, that the sums ∑ j, a x j and ∑ j, b y j are positive, is not part of this statement.