← Mathematical handbook

Equality in the decreasing-function moment bound

The nonnegative defect |g(u)-g(w)|-(g(u)-g(w))^2 vanishes precisely when each difference is zero or has absolute value one. Consequently a bounded function is either constant or binary almost everywhere.

def Verification.pairMomentDefect (x y : ℝ) : ℝ

Equations

• Verification.pairMomentDefect x y = |x - y| - (x - y) ^ 2

theorem Verification.pairMomentDefect_mem_Icc {x y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) : pairMomentDefect x y ∈ Set.Icc 0 1

theorem Verification.integrable_pairMomentDefect {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : MeasureTheory.Integrable (fun (p : ↑unitInterval × ↑unitInterval) => pairMomentDefect (g p.1) (g p.2)) (MeasureTheory.volume.prod MeasureTheory.volume)

theorem Verification.integral_sq_sub_unit {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (c : ℝ) : ∫ (w : ↑unitInterval), (c - g w) ^ 2 = (c ^ 2 - 2 * c * ∫ (w : ↑unitInterval), g w) + ∫ (w : ↑unitInterval), g w ^ 2

theorem Verification.integral_integral_sq_sub_unit {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval) (w : ↑unitInterval), (g u - g w) ^ 2 = (2 * ∫ (u : ↑unitInterval), g u ^ 2) - 2 * (∫ (u : ↑unitInterval), g u) ^ 2

theorem Verification.integral_integral_abs_sub_of_antitone {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval) (w : ↑unitInterval), |g u - g w| = (4 * ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w) - 2 * ∫ (u : ↑unitInterval), g u

theorem Verification.integral_pairMomentDefect {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval) (w : ↑unitInterval), pairMomentDefect (g u) (g w) = 2 * (((2 * ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w) - ∫ (u : ↑unitInterval), g u) + (∫ (u : ↑unitInterval), g u) ^ 2 - ∫ (u : ↑unitInterval), g u ^ 2)

theorem Verification.ae_constant_or_binary_of_pair_defect_zero {g : ↑unitInterval → ℝ} (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (hz : ∀ᵐ (u : ↑unitInterval) (w : ↑unitInterval), pairMomentDefect (g u) (g w) = 0) : (∀ᵐ (u : ↑unitInterval), g u = ∫ (w : ↑unitInterval), g w) ∨ ∀ᵐ (u : ↑unitInterval), g u = 0 ∨ g u = 1

theorem Verification.ae_constant_or_binary_of_moment_eq {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (he : ∫ (u : ↑unitInterval), g u ^ 2 = ((2 * ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w) - ∫ (u : ↑unitInterval), g u) + (∫ (u : ↑unitInterval), g u) ^ 2) : (∀ᵐ (u : ↑unitInterval), g u = ∫ (w : ↑unitInterval), g w) ∨ ∀ᵐ (u : ↑unitInterval), g u = 0 ∨ g u = 1

theorem Verification.ae_lower_indicator_of_antitone_binary {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), g u = ↑v) (hbin : ∀ᵐ (u : ↑unitInterval), g u = 0 ∨ g u = 1) : g =ᵐ[MeasureTheory.volume] (Set.Iic v).indicator fun (x : ↑unitInterval) => 1

An antitone binary function with mean v is the lower-interval indicator, up to the unavoidable null-set ambiguity.

theorem Verification.moment_eq_iff_ae_constant_or_lower_indicator {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), g u = ↑v) : ∫ (u : ↑unitInterval), g u ^ 2 = (2 * ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w) - ↑v + ↑v ^ 2 ↔ (∀ᵐ (u : ↑unitInterval), g u = ↑v) ∨ g =ᵐ[MeasureTheory.volume] (Set.Iic v).indicator fun (x : ↑unitInterval) => 1

Equality in the moment inequality, with equality of functions interpreted almost everywhere, as required for integral statements.