English
If g is integrable and strongly measurable of the supremum filtration, then eLpNorm of the difference between conditional expectations and g tends to zero in L¹ along the filtration, i.e., convergence of condExp to g in L¹.
Русский
Если g интегрируем и сильно измерима относительно супремы фильтраций, то норма eLpNorm разности между condExp и g сходится к нулю в L¹.
LaTeX
$$$\\mathrm{tendsto}_{n\\to\\infty} \\, \\mathrm{eLpNorm}(\\mu[g|\\mathcal{F}_n] - g, 1, \\mu) = 0.$$$
Lean4
/-- **Lévy's upward theorem**, almost everywhere version: given a function `g` and a filtration
`ℱ`, the sequence defined by `𝔼[g | ℱ n]` converges almost everywhere to `𝔼[g | ⨆ n, ℱ n]`. -/
theorem tendsto_ae_condExp (g : Ω → ℝ) : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[g|ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ℱ n]) x)) :=
by
have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ℱ n]) x)) :=
integrable_condExp.tendsto_ae_condExp stronglyMeasurable_condExp
have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x = (μ[g|ℱ n]) x := fun n =>
condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
rw [← ae_all_iff] at heq
filter_upwards [heq, ht] with x hxeq hxt
exact hxt.congr hxeq
