English
Lévy’s upward theorem states that the conditional expectations μ[g|ℱ n] converge in a suitable sense to μ[g|⨆ n,ℱ n] as n → ∞.
Русский
У леви вверх-твердение утверждает, что условные ожидания μ[g|ℱ n] сходятся к μ[g|⨆ n,ℱ n] по мере продвижения n.
LaTeX
$$$\\lim_{n\\to\\infty} μ[g|ℱ n] = μ[g|⨆ n,ℱ n] \\quad \\text{in appropriate sense.}$$$
Lean4
/-- If a martingale `f` adapted to `ℱ` converges in L¹ to `g`, then for all `n`, `f n` is almost
everywhere equal to `𝔼[g | ℱ n]`. -/
theorem eq_condExp_of_tendsto_eLpNorm {μ : Measure Ω} (hf : Martingale f ℱ μ) (hg : Integrable g μ)
(hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)) (n : ℕ) : f n =ᵐ[μ] μ[g|ℱ n] :=
by
rw [← sub_ae_eq_zero, ←
eLpNorm_eq_zero_iff
(((hf.stronglyMeasurable n).mono (ℱ.le _)).sub (stronglyMeasurable_condExp.mono (ℱ.le _))).aestronglyMeasurable
one_ne_zero]
have ht : Tendsto (fun m => eLpNorm (μ[f m - g|ℱ n]) 1 μ) atTop (𝓝 0) :=
haveI hint : ∀ m, Integrable (f m - g) μ := fun m => (hf.integrable m).sub hg
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hgtends (fun m => zero_le _) fun m =>
eLpNorm_one_condExp_le_eLpNorm _
have hev : ∀ m ≥ n, eLpNorm (μ[f m - g|ℱ n]) 1 μ = eLpNorm (f n - μ[g|ℱ n]) 1 μ :=
by
refine fun m hm => eLpNorm_congr_ae ((condExp_sub (hf.integrable m) hg _).trans ?_)
filter_upwards [hf.2 n m hm] with x hx
simp only [hx, Pi.sub_apply]
exact tendsto_nhds_unique (tendsto_atTop_of_eventually_const hev) ht
