The third-moment inequality

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. Then, for every real s,

E[((f - s)⁺)^3] · Pr[f ≤ s] ≤ (3/2) K² M

(Theorem 7.6 of the paper; thirdMoment_of_integratedAllPairs : IntegratedAllPairsInequality → ThirdMomentInequality; the unnormalised form is Level.thirdMoment_core).

Proof: in the integrated all-pairs inequality (Proposition 7.4) keep the pairs (x, y) with f y ≤ s < f x, where (f x - f y)^3 ≥ (f x - s)^3. Dividing the row at x by (f x - s)^3 turns the inequality into the hypothesis of the lemma that removes the weights (Lemma 5.3 of the paper; abstract_cs in TwoSided/CauchySchwarz.lean), whose conclusion is the claim.

Two consequences of the third-moment inequality:

• Level.thirdMoment_lower — the inequality on the other side, E[((s - f)⁺)^3] · Pr[f ≥ s] ≤ (3/2) K² M (the second inequality of Theorem 7.6);
• Level.separated_sets — if f ≥ s + θ on A and f ≤ s on B, then 2 θ^3 μ(A) μ(B) ≤ 3 K² M (Corollary 7.7).

theorem AaronsonAmbainis.Level.four_mul_integrated {ι : Type} [Fintype ι] [DecidableEq ι] (hInt : IntegratedAllPairsInequality) (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, so that 4^n appears in place of 4^(n-1) (for n = 0 both sides are 0).

theorem AaronsonAmbainis.Level.thirdMoment_core {ι : Type} [Fintype ι] [DecidableEq ι] (hInt : IntegratedAllPairsInequality) (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) (s : ℝ) : (∑ x : Cube ι, max (f x - s) 0 ^ 3) * ↑{y : Cube ι | f y ≤ s}.card ≤ 3 / 2 * 4 ^ Fintype.card ι * M * K ^ 2

The third-moment inequality, unnormalised: (∑_x ((f x - s)⁺)^3) · #{y : f y ≤ s} ≤ (3/2) 4^n M K².

theorem AaronsonAmbainis.thirdMoment_of_integratedAllPairs : IntegratedAllPairsInequality → ThirdMomentInequality

The third-moment inequality (Theorem 7.6 of the paper, first inequality) from the integrated all-pairs inequality (Proposition 7.4).

theorem AaronsonAmbainis.Level.thirdMoment_lower {ι : 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) (s : ℝ) : (∑ x : Cube ι, max (s - f x) 0 ^ 3) / 2 ^ Fintype.card ι * (↑{y : Cube ι | s ≤ f y}.card / 2 ^ Fintype.card ι) ≤ 3 / 2 * K ^ 2 * M

The third-moment inequality on the other side (Theorem 7.6 of the paper, second inequality): E[((s - f)⁺)^3] · Pr[f ≥ s] ≤ (3/2) K² M. It is the third-moment inequality for -f and -s.

theorem AaronsonAmbainis.Level.separated_sets {ι : 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) (A B : Finset (Cube ι)) (s θ : ℝ) (hθ : 0 ≤ θ) (hA : ∀ x ∈ A, s + θ ≤ f x) (hB : ∀ y ∈ B, f y ≤ s) : 2 * θ ^ 3 * (↑A.card / 2 ^ Fintype.card ι) * (↑B.card / 2 ^ Fintype.card ι) ≤ 3 * K ^ 2 * M

Two separated sets (Corollary 7.7 of the paper). If f has rows of cost at most K everywhere, M ≥ 0 bounds all L_j = meanAbsIncr f j, and f ≥ s + θ on A, f ≤ s on B with θ ≥ 0, then 2 θ^3 μ(A) μ(B) ≤ 3 K² M (μ the uniform probability on the cube).