English
Under IsFiniteMeasure μ, for a submartingale f adapted to ℱ with bounded L1, the limit process is the almost-sure limit of f.
Русский
При конечной мере μ, субмартингал f, адаптированный к ℱ, имеет в предельном процессе почти верный предел лимита.
LaTeX
$$$\\forall^{a.e.} \\omega,\\; f_n(\\omega) \\to \\mathcal{F}.\\mathrm{limitProcess}(f,\\mu,ω).$$$
Lean4
/-- Part a of the **L¹ martingale convergence theorem**: a uniformly integrable submartingale
adapted to the filtration `ℱ` converges a.e. and in L¹ to an integrable function which is
measurable with respect to the σ-algebra `⨆ n, ℱ n`. -/
theorem tendsto_eLpNorm_one_limitProcess (hf : Submartingale f ℱ μ) (hunif : UniformIntegrable f 1 μ) :
Tendsto (fun n => eLpNorm (f n - ℱ.limitProcess f μ) 1 μ) atTop (𝓝 0) :=
by
obtain ⟨R, hR⟩ := hunif.2.2
have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable
exact
tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hmeas (memLp_limitProcess_of_eLpNorm_bdd hmeas hR)
hunif.2.1 (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)
