Finiteness of the Maximal $L^p$ Integral

This auxiliary lemma transfers finiteness from a submartingale terminal value to its running maximum.

Let $f$ be a nonnegative submartingale under a finite measure, let $p>1$, and fix $n\in\mathbb N$. If

then

where $f_n^\ast$ is the maximum of $f_k$ for $k\leq n$. The integrals are ENNReal lower integrals of ENNReal.ofReal powers.

This result supplies the finiteness needed to pass from truncated maximal estimates to the untruncated setting.

Original Lean declaration header

Within namespace MeasureTheory. Shown in its original module context. Proof omitted.

private lemma runMax_pow_lintegral_lt_top
    [IsFiniteMeasure μ] {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} {p : ℝ}
    (hsub : Submartingale f 𝒢 μ) (hnonneg : ∀ n ω, 0 ≤ f n ω) (hp : 1 < p) (n : ℕ)
    (hB_lt_top : ∫⁻ ω, ENNReal.ofReal ((f n ω) ^ p) ∂μ < ⊤) :
    ∫⁻ ω, ENNReal.ofReal ((runMax f n ω) ^ p) ∂μ < ⊤

Module navigation

Module: MathFin/Foundations/DoobLpMaximalInequality.

Supporting theorems: holder_step_truncated.

Previous: holder_step · Next: maximal_ineq_Lp.

Source excerpt, lines 844–848 · Frozen source 408915f.