theorem
unifIntegrable_p_at_p_of_submartingale
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{p : ENNReal}
(hp : 1 < p)
(hp_top : p ≠ ⊤)
(hsub : MeasureTheory.Submartingale f ℱ μ)
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
{R : NNReal}
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
Auxiliary lemma: if a submartingale f on a probability space has
L^p-norms uniformly bounded by R for some 1 < p < ∞, then the family
f is L^p-uniformly integrable. Used in the proof of the L^p martingale
convergence theorem (Lecture 28).
theorem
martingale_Lp_convergence_ae
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{ℱ : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{p : ENNReal}
{R : NNReal}
(hsub : MeasureTheory.Submartingale f ℱ μ)
(hp1 : 1 < p)
(hp_top : p ≠ ⊤)
(hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R)
:
(∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess f ℱ μ ω))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - MeasureTheory.Filtration.limitProcess f ℱ μ) p μ)
Filter.atTop (nhds 0)
L^p martingale convergence theorem (Lecture 28): if f is a submartingale
on a probability space with sup_n ‖f n‖_p < ∞ for some 1 < p < ∞, then
f n converges almost surely to a limit process X, and moreover the
convergence holds in L^p (i.e. ‖f n - X‖_p → 0).