English
The limiting process of an Lp-bounded submartingale lies in Lp, under sigma-finiteness and adaptedness assumptions.
Русский
Предел процесса подмартингала в Lp принадлежит Lp, при условии сигма-финичности и адаптированности.
LaTeX
$$$\\mathrm{MemLp}(\\mathcal{F}.\\mathrm{limitProcess}(f,\\mu),p,\\mu).$$$
Lean4
/-- Part c of the **L¹ martingale convergence theorem**: Given an integrable function `g` which
is measurable with respect to `⨆ n, ℱ n` where `ℱ` is a filtration, the martingale defined by
`𝔼[g | ℱ n]` converges in L¹ to `g`.
This martingale also converges to `g` almost everywhere and this result is provided by
`MeasureTheory.Integrable.tendsto_ae_condExp` -/
theorem tendsto_eLpNorm_condExp (hg : Integrable g μ) (hgmeas : StronglyMeasurable[⨆ n, ℱ n] g) :
Tendsto (fun n => eLpNorm (μ[g|ℱ n] - g) 1 μ) atTop (𝓝 0) :=
tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top
(fun n => (stronglyMeasurable_condExp.mono (ℱ.le n)).aestronglyMeasurable) (memLp_one_iff_integrable.2 hg)
hg.uniformIntegrable_condExp_filtration.2.1
(tendstoInMeasure_of_tendsto_ae (fun n => (stronglyMeasurable_condExp.mono (ℱ.le n)).aestronglyMeasurable)
(hg.tendsto_ae_condExp hgmeas))
