The L¹ norm is dominated by the L² norm on a probability space
ProvedProbabilityTheory.integral_abs_le_sqrt_integral_sqCauchy-Schwarz against the constant . On a probability space,
Where this is used. In the truncation argument for the Markov chain central limit theorem, the available control on is a second-moment bound coming from the variance estimate for partial sums, whereas the approximation lemma that closes the argument consumes a first-moment bound. This inequality is the bridge, and it is the reason the final approximation error is rather than something involving an modulus.
Proof. Rather than invoking the Cauchy-Schwarz inequality, use the elementary weighted arithmetic-geometric bound: for every and every real ,
which is just divided by . Integrating gives for every . If , choosing makes the right-hand side exactly . If then almost everywhere, hence almost everywhere and both sides vanish. (Integrability of itself follows from that of on a probability space.)
import Mathlib.MeasureTheory.Integral.Bochner.Set import Mathlib.Analysis.SpecialFunctions.Sqrt open Filter MeasureTheory ProbabilityTheory open scoped ENNReal NNReal Topology
theorem ProbabilityTheory.integral_abs_le_sqrt_integral_sq {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ] (Z : Ω → ℝ) (hZ : Measurable Z)
(hsq : Integrable (fun ω => (Z ω) ^ 2) μ) :
∫ ω, |Z ω| ∂μ ≤ Real.sqrt (∫ ω, (Z ω) ^ 2 ∂μ) := by sorry