English
In Lévy's upward theorem for L¹, the sequence of conditional expectations μ[g|ℱ n] converges in L¹ to μ[g|⨆ n,ℱ n] as n grows, i.e., Tendsto of the L¹-norm difference to 0.
Русский
В теореме Лёвиа сверху (L¹) последовательность условных ожиданий μ[g|ℱ n] сходится в L¹ к μ[g|⨆ n,ℱ n].
LaTeX
$$$\\lim_{n\\to\\infty} \\| μ[g|ℱ n] - μ[g|⨆ n,ℱ n] \\|_{L^1(μ)} = 0.$$$
Lean4
/-- **Lévy's upward theorem**, L¹ version: given a function `g` and a filtration `ℱ`, the
sequence defined by `𝔼[g | ℱ n]` converges in L¹ to `𝔼[g | ⨆ n, ℱ n]`. -/
theorem tendsto_eLpNorm_condExp (g : Ω → ℝ) : Tendsto (fun n => eLpNorm (μ[g|ℱ n] - μ[g|⨆ n, ℱ n]) 1 μ) atTop (𝓝 0) :=
by
have ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ℱ n]|ℱ n] - μ[g|⨆ n, ℱ n]) 1 μ) atTop (𝓝 0) :=
integrable_condExp.tendsto_eLpNorm_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)
refine ht.congr fun n => eLpNorm_congr_ae ?_
filter_upwards [heq n] with x hxeq
simp only [hxeq, Pi.sub_apply]
