The integrated all-pairs inequality

Let f be a real function on the cube with a row a x at every point x, and let w > 0. Integrating the all-pairs inequality at the level t (level_allPairs) over all real t (level_integration) gives the integrated all-pairs inequality (Proposition 7.4 of the paper):

∑_{(x,y) : f y < f x} (f x - f y)^3 / (6 s_xy) ≤ 4^(n-1) ∑_j L_j / w_j, s_xy = ∑_{j ∈ Δ(x,y)} w_j a^x_j a^y_j, L_j = meanAbsIncr f j = E_x |f x - f (x^j)|.

• Level.integrated_core — the form that comes out of the integration;
• Level.integrated_four_mul — multiplied by 4, so that 4^n appears;
• integratedAllPairs_of_allPairs : AllPairsInequality → IntegratedAllPairsInequality — with 4^(n-1) as printed above (for n = 0 both sides are 0).

The denominators are positive: Level.pairSum_pos in Level/AllPairs.lean.

theorem AaronsonAmbainis.Level.integrated_core {ι : Type} [Fintype ι] [DecidableEq ι] (hAllPairs : AllPairsInequality) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (w : ι → ℝ) (hw : ∀ (j : ι), 0 < w j) : 2 * ∑ x : Cube ι, ∑ y : Cube ι, max (f x - f y) 0 ^ 3 / 6 * (∑ j ∈ diffSet x y, w j * a x j * a y j)⁻¹ ≤ 2 ^ Fintype.card ι * ∑ j : ι, (∑ x : Cube ι, max (f x - f (flipSet x {j})) 0) / w j

The integrated all-pairs inequality, in the form that comes out of the integration over the level.

theorem AaronsonAmbainis.Level.sum_posPart_incr {ι : Type} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : ∑ x : Cube ι, max (f x - f (flipSet x {j})) 0 = (∑ x : Cube ι, |f x - f (flipSet x {j})|) / 2

∑_x (f x - f (x^j))⁺ = (1/2) ∑_x |f x - f (x^j)| (Lemma 7.3 (iii) of the paper).

theorem AaronsonAmbainis.Level.integrated_four_mul {ι : Type} [Fintype ι] [DecidableEq ι] (hAllPairs : AllPairsInequality) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (w : ι → ℝ) (hw : ∀ (j : ι), 0 < w j) : 4 * ∑ x : Cube ι, ∑ y : Cube ι with f y < f x, (f x - f y) ^ 3 / (6 * ∑ j ∈ diffSet x y, w j * a x j * a y j) ≤ 4 ^ Fintype.card ι * ∑ j : ι, meanAbsIncr f j / w j

The integrated all-pairs inequality, multiplied by 4: for a real function f on the cube, rows a x of f and weights w > 0, 4 ∑_{(x,y) : f y < f x} (f x - f y)^3 / (6 ∑_{j ∈ Δ(x,y)} w_j a^x_j a^y_j) ≤ 4^n ∑_j L_j / w_j, where L_j = meanAbsIncr f j = E_x |f x - f (x^j)|.

theorem AaronsonAmbainis.integratedAllPairs_of_allPairs : AllPairsInequality → IntegratedAllPairsInequality

The integrated all-pairs inequality (Proposition 7.4 of the paper) from the all-pairs inequality for Boolean functions (Proposition 5.2).