The all-pairs inequality at one level

Let f be a real function on the cube with a row a x at every point x, and let t be a real number. The all-pairs inequality (Proposition 5.2 of the paper), applied to the level function g_t = 1_{f > t} with the rows a x / |f x - t| (levRow, Lemma 2.4 (iii) of the paper), reads

2 ∑_x ∑_y (f x - t)⁺ (t - f y)⁺ / s_xy ≤ 2^n ∑_j b_j(g_t) / w_j, s_xy = ∑_{j ∈ Δ(x,y)} w_j a^x_j a^y_j

(level_allPairs; Lemma 7.2 of the paper, multiplied by 2), for every real t. Also: s_xy > 0 when f y < f x (pairSum_pos; Lemma 7.1), and b_j(g_t) is the number of points x with f(x^j) ≤ t < f(x) (bdry_lev).

theorem AaronsonAmbainis.Level.sum_levRow {ι : Type} [Fintype ι] (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (w : ι → ℝ) {t : ℝ} {x y : Cube ι} (hx : t < f x) (hy : f y < t) : ∑ j ∈ diffSet x y, w j * levRow f a t x j * levRow f a t y j = (∑ j ∈ diffSet x y, w j * a x j * a y j) / ((f x - t) * (t - f y))

The overlap sum of the level rows at a point above the level and a point below it (Lemma 7.1 (i) of the paper).

theorem AaronsonAmbainis.Level.pairSum_pos {ι : Type} [Fintype ι] {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) {x y : Cube ι} (hxy : f y < f x) : 0 < ∑ j ∈ diffSet x y, w j * a x j * a y j

Rows at two points with different values overlap on the difference set: s_xy > 0 (Lemma 7.1 (ii) of the paper).

theorem AaronsonAmbainis.Level.level_allPairs {ι : 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) (t : ℝ) : 2 * ∑ x : Cube ι, ∑ y : Cube ι, max (f x - t) 0 * max (t - f y) 0 * (∑ j ∈ diffSet x y, w j * a x j * a y j)⁻¹ ≤ 2 ^ Fintype.card ι * ∑ j : ι, ↑(bdry (lev f t) j) / w j

The all-pairs inequality at the level t (Lemma 7.2 of the paper, multiplied by 2), from the all-pairs inequality for Boolean functions.

theorem AaronsonAmbainis.Level.bdry_lev {ι : Type} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (t : ℝ) (j : ι) : ↑(bdry (lev f t) j) = ∑ x : Cube ι, if f (flipSet x {j}) ≤ t ∧ t < f x then 1 else 0

b_j(g_t) is the number of points x with f(x^j) ≤ t < f(x).