Fubini Swap for the Maximal Layer Integral

This auxiliary lemma performs the Fubini step for a nonnegative submartingale.

Let $f:\mathbb N\times\Omega\to\mathbb R$ be a nonnegative submartingale with respect to a filtration $\mathcal G$ and a finite measure $\mu$, let $p>1$, and fix $n\in\mathbb N$. Then

where $f_n^\ast$ is the discrete running maximum.

This is a technical Fubini identity used in the strong Doob $L^p$ estimate.

Formalization Note. The displayed integrals are represented as ENNReal lower integrals with ofReal coercions.

Original Lean declaration header

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

private lemma fubini_swap
    [IsFiniteMeasure μ] {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} {p : ℝ}
    (hsub : Submartingale f 𝒢 μ) (hnonneg : ∀ n ω, 0 ≤ f n ω)
    (hp : 1 < p) (n : ℕ) :
    ∫⁻ t in Set.Ioi (0:ℝ),
        ENNReal.ofReal (t ^ (p - 2)) *
          ∫⁻ ω in {ω | t ≤ runMax f n ω}, ENNReal.ofReal (f n ω) ∂μ
      = ∫⁻ ω, ENNReal.ofReal (f n ω) *
              ENNReal.ofReal ((runMax f n ω) ^ (p - 1) / (p - 1)) ∂μ

Module navigation

Module: MathFin/Foundations/DoobLpMaximalInequality.

Supporting theorems: inner_t_integral.

Previous: inner_t_integral · Next: fubini_swap_truncated.

Source excerpt, lines 201–209 · Frozen source 408915f.