Theorems · Theorem · probability

MeasureTheory.maximal_ineq

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f 𝒢 μ →
    0 ≤ f →
      ∀ {ε : NNReal} (n : ℕ),
        ↑ε * μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤
          ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω}, f n ω ∂μ)

Doob's maximal inequality: Given a non-negative submartingale f, for all ε : ℝ≥0, we have ε • μ {ε ≤ f* n} ≤ ∫ ω in {ε ≤ f* n}, f n where f* n ω = max_{k ≤ n}, f k ω. In some literature, the Doob's maximal inequality refers to what we call Doob's Lp inequality (which is a corollary of this lemma and will be proved in an upcoming PR).

Defined in

Mathlib.Probability.Martingale.OptionalStopping

Cited by

0 results in Mathlib

Foundations

Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasure