The two-sided inequality from the all-pairs inequality (twoSided_of_allPairs)

Section 5.2 of the paper (the proof of Theorem 5.4).

From the all-pairs inequality and bdry g j = 2 ^ n * infl g j / 2 ≤ 2 ^ n * τ / 2:

∑_{x ∈ O} ∑_{y ∈ N} (∑_{j ∈ Δ(x,y)} w j * lam x j * lam y j)⁻¹ ≤ (4 ^ n * τ / 4) * ∑ j, (w j)⁻¹

for every positive weight vector w (O = {g = true}, N = {g = false}). The lemma that removes the weights (Lemma 5.3, abstract_cs in the file CauchySchwarz.lean) gives (∑_{x ∈ O} ‖lam x‖₁⁻¹) * (∑_{y ∈ N} ‖lam y‖₁⁻¹) ≤ 4 ^ n * τ / 4; the overlap lemma (file Overlap.lean) supplies the positivity of the denominators.

theorem AaronsonAmbainis.final_arith {VO VN T τ : ℝ} (hT : 0 < T) (h : VO * VN ≤ T * T * τ / 4) : 4 * (VO / T) * (VN / T) ≤ τ

The final arithmetic: VO * VN ≤ T * T * τ / 4 gives 4 * (VO / T) * (VN / T) ≤ τ.

theorem AaronsonAmbainis.twoSided_of_allPairs : AllPairsInequality → TwoSidedInequality

The two-sided inequality (the inequality of Theorem 5.4 of the paper) from the all-pairs inequality (Proposition 5.2).