First-Moment Bound from an Extended $L^2$ Bound

This is a probability-space $L^2$-to-$L^1$ estimate.

Let $P$ be a probability measure on $\Omega$, let $g:\Omega\to\mathbb R$ be almost everywhere strongly measurable, and let $V\ge0$. If

where the left side is the extended nonnegative integral, then $g$ is integrable and

This is a reusable conversion from an extended-valued squared-moment estimate to integrability and an ordinary first-moment estimate.

Formalization Note The hypothesis uses ENNReal and ENNReal.ofReal; the conclusion uses the ordinary integral and Real.sqrt.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem integral_abs_le_sqrt_of_lintegral_sq_le {P : Measure Ω} [IsProbabilityMeasure P]
    {g : Ω → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g P) {V : ℝ} (hV0 : 0 ≤ V)
    (hle : ∫⁻ ω, (‖g ω‖₊ : ℝ≥0∞) ^ 2 ∂P ≤ ENNReal.ofReal V) :
    MeasureTheory.Integrable g P ∧ ∫ ω, |g ω| ∂P ≤ Real.sqrt V

Module navigation

Module: LevyStochCalc/Brownian/ItoFormulaScalar.

Supporting theorems: integral_abs_le_sqrt_of_integral_sq_le.

Source excerpt, lines 52–55 · Frozen source 408915f.