Theorems · Theorem · probability

MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    MeasureTheory.UniformIntegrable f 1 μ →
      Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - MeasureTheory.Filtration.limitProcess f ℱ μ) 1 μ)
        Filter.atTop (nhds 0)

Part a of the L¹ martingale convergence theorem: a uniformly integrable submartingale strongly adapted to the filtration ℱ converges a.e. and in L¹ to an integrable function which is measurable with respect to the σ-algebra ⨆ n, ℱ n.

Defined in

Mathlib.Probability.Martingale.Convergence

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure