noncomputable def MeasureTheory.maxProcess {Ω : Type u_1} (f : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ

The running maximum of |f k ω| over 0 ≤ k ≤ n, i.e. maxProcess f n ω = max_{0 ≤ k ≤ n} |f k ω|.

noncomputable def MeasureTheory.predictableQuadraticVariation {Ω : Type u_1} {m0 : MeasurableSpace Ω} (μ : Measure Ω) (ℱ : Filtration ℕ m0) (f : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ

The predictable quadratic variation of f with respect to ℱ and μ, defined pointwise by A_n(ω) = ∑_{k=0}^{n-1} E[(f_{k+1} - f_k)² | ℱ_k] (ω).

theorem MeasureTheory.doob_sq_maximal_ineq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [IsProbabilityMeasure μ] (hmart : Martingale f ℱ μ) (hL2 : ∀ (n : ℕ), MemLp (f n) 2 μ) (n : ℕ) : ∫ (ω : Ω), maxProcess f n ω ^ 2 ∂μ ≤ 4 * ∫ (ω : Ω), predictableQuadraticVariation μ ℱ f n ω ∂μ

Square integrable martingale maximal inequality (finite horizon). For a square-integrable martingale Xₙ, the expected square of max_{0 ≤ k ≤ n} |X_k| is bounded by 4 · E[A_n], where A_n = ∑_{k<n} E[(X_{k+1} - X_k)² | ℱ_k] is the predictable quadratic variation.

theorem MeasureTheory.doob_sq_maximal_ineq_iSup {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [IsProbabilityMeasure μ] (hmart : Martingale f ℱ μ) (hL2 : ∀ (n : ℕ), MemLp (f n) 2 μ) : ∫⁻ (ω : Ω), ⨆ (n : ℕ), ENNReal.ofReal (|f n ω| ^ 2) ∂μ ≤ 4 * ∫⁻ (ω : Ω), ⨆ (n : ℕ), ENNReal.ofReal (predictableQuadraticVariation μ ℱ f n ω) ∂μ

Square integrable martingale maximal inequality (infinite horizon). For a square-integrable martingale Xₙ, E[sup_n |X_n|²] ≤ 4 · E[A_∞], where A_∞ = ∑_{k≥0} E[(X_{k+1} - X_k)² | ℱ_k]. This is the ENNReal-valued form applicable to the supremum over all n.