The mean absolute increments: from the third-moment inequality to the variance

Let f be a real function on the cube with rows of cost at most K at every point, and let M ≥ 0 bound all the mean absolute increments L_j = meanAbsIncr f j. With a median m of f, the third-moment inequality and the inequality on the other side (Level.thirdMoment_lower) give E|f - m|^3 ≤ 6 K² M (Level.exists_abs_cube_le). Since Var f ≤ E (f - m)² and (E z²)^3 ≤ (E |z|^3)^2, it follows that

Var(f)^3 ≤ 36 K^4 M² (Level.variance_cube_le).

Taking M = max_j L_j (Theorem 7.10 of the paper):

• meanIncrement_of_thirdMoment : ThirdMomentInequality → MeanIncrementBound — some j has Var(f)^3 ≤ 36 K^4 L_j²;
• Level.exists_meanAbsIncr_ge_sqrt — the same with the power 3/2 written as Var · √Var: Var(f)^{3/2} ≤ 6 K² L_j (the two forms are equivalent: Level.cube_le_iff_mul_sqrt_le).

No bound on the values of f is used. That K > 0 under these hypotheses is Level.cost_pos.

theorem AaronsonAmbainis.Level.exists_abs_cube_le {ι : Type} [Fintype ι] [DecidableEq ι] (hTM : ThirdMomentInequality) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) {K : ℝ} (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ (j : ι), meanAbsIncr f j ≤ M) : ∃ (m : ℝ), (∑ x : Cube ι, |f x - m| ^ 3) / 2 ^ Fintype.card ι ≤ 6 * K ^ 2 * M

E|f - m|^3 ≤ 6 K² M for a median m of f.

theorem AaronsonAmbainis.Level.variance_cube_le {ι : Type} [Fintype ι] [DecidableEq ι] (hTM : ThirdMomentInequality) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) {K : ℝ} (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ (j : ι), meanAbsIncr f j ≤ M) : variance f ^ 3 ≤ 36 * K ^ 4 * M ^ 2

Var(f)^3 ≤ 36 K^4 M² when f has rows of cost at most K everywhere and M ≥ 0 bounds all the mean absolute increments L_j = meanAbsIncr f j.

theorem AaronsonAmbainis.meanIncrement_of_thirdMoment : ThirdMomentInequality → MeanIncrementBound

The bound for the mean absolute increments (Theorem 7.10 of the paper) from the third-moment inequality (Theorem 7.6): if Var(f) > 0 and f has rows of cost at most K everywhere, then some coordinate j has Var(f)^3 ≤ 36 K^4 L_j², where L_j = meanAbsIncr f j = E|f(x) - f(x^j)|.

theorem AaronsonAmbainis.Level.cube_le_iff_mul_sqrt_le {V K L : ℝ} (hV : 0 ≤ V) (hL : 0 ≤ L) : V ^ 3 ≤ 36 * K ^ 4 * L ^ 2 ↔ V * √V ≤ 6 * K ^ 2 * L

For V, L ≥ 0: V^3 ≤ 36 K^4 L² if and only if V^{3/2} ≤ 6 K² L, where V^{3/2} is written V · √V.

theorem AaronsonAmbainis.Level.exists_meanAbsIncr_ge_sqrt {ι : Type} [Fintype ι] [DecidableEq ι] (hMI : MeanIncrementBound) (f : Cube ι → ℝ) (a : Cube ι → ι → ℝ) (ha : ∀ (x : Cube ι) (j : ι), 0 ≤ a x j) {K : ℝ} (hsum : ∀ (x : Cube ι), ∑ j : ι, a x j ≤ K) (hrow : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ j ∈ diffSet x y, a x j) (hvar : 0 < variance f) : ∃ (j : ι), variance f * √(variance f) ≤ 6 * K ^ 2 * meanAbsIncr f j

The bound for the mean absolute increments with the power 3/2 written as Var · √Var: some coordinate j has Var(f)^{3/2} ≤ 6 K² L_j, that is, L_j ≥ Var(f)^{3/2} / (6 K²).