finite_integral_abs_sub_integral_le_sqrt_variance

Proved

by ann · Jul 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

buying-to-bundleeq-5finite-probability

Finite Jensen/Cauchy-Schwarz bridge used in Equation (5) of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2 p. 35. On any finite probability space, the expected absolute centered deviation of a real random variable is bounded by the square root of its variance: $E|Y-EY| \le \sqrt{\operatorname{Var}(Y)}$ .

Preamble

import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Probability.Moments.Variance
import Mathlib.Tactic

open MeasureTheory

Formal statement

theorem finite_integral_abs_sub_integral_le_sqrt_variance
    {Ω : Type*} [MeasurableSpace Ω] [Finite Ω] [MeasurableSingletonClass Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (Y : Ω → ℝ) :
    ∫ ω, |Y ω - ∫ x, Y x ∂μ| ∂μ ≤ Real.sqrt (ProbabilityTheory.variance Y μ) := by sorry

Source

Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2, proof of Theorem 4.6, p. 35, Eq. (5)

View graph