Doob’s Discrete-Time $L^p$ Maximal Inequality

This formalizes Doob’s strong-type maximal inequality for discrete-time submartingales.

Let $(\Omega,\mathcal F,\mu)$ be a finite measure space, let $\mathcal G$ be a filtration indexed by $\mathbb N$, let $f_n:\Omega\to\mathbb R$ be a $\mathcal G$-submartingale, and let $p\in\mathbb R$ satisfy $1<p$. Assume $f_n(\omega)\ge 0$ for every $n$ and $\omega$. For each $n$, define the running maximum $f_n^*(\omega)=\max_{0\le k\le n}f_k(\omega)$.

The Lean statement uses eLpNorm with exponent ENNReal.ofReal p; thus both sides are values in $[0,\infty]$, and the running maximum is represented by a finite supremum. This is a reusable strong-type maximal estimate.

Original Lean declaration header

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

theorem maximal_ineq_Lp
    [IsFiniteMeasure μ] {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} {p : ℝ}
    (hsub : Submartingale f 𝒢 μ) (hnonneg : ∀ n ω, 0 ≤ f n ω)
    (hp : 1 < p) (n : ℕ) :
    eLpNorm (fun ω ↦ (Finset.range (n + 1)).sup' Finset.nonempty_range_add_one
        (fun k ↦ f k ω)) (ENNReal.ofReal p) μ
      ≤ ENNReal.ofReal (p / (p - 1)) *
          eLpNorm (f n) (ENNReal.ofReal p) μ

Module navigation

Module: MathFin/Foundations/DoobLpMaximalInequality.

Supporting theorems: holder_step, runMax_pow_lintegral_lt_top.

Previous: runMax_pow_lintegral_lt_top.

Source excerpt, lines 939–946 · Frozen source 408915f.