English
If f is a uniformly integrable martingale adapted to ℱ, then for all n, f_n is a.e. equal to the conditional expectation of the limitProcess with respect to ℱ n.
Русский
Если f является униформно интегрируемым мартингалом, адаптированным к ℱ, то для каждого n верно f_n = a.e. E[g|ℱ n] с g = limitProcess.
LaTeX
$$$f_n =_{a.e.} \\mathbb{E}[\\mathrm{limitProcess}(f,\\mu) | \\mathcal{F}_n].$$$
Lean4
/-- Part b of the **L¹ martingale convergence theorem**: if `f` is a uniformly integrable martingale
adapted to the filtration `ℱ`, then for all `n`, `f n` is almost everywhere equal to the conditional
expectation of its limiting process w.r.t. `ℱ n`. -/
theorem ae_eq_condExp_limitProcess (hf : Martingale f ℱ μ) (hbdd : UniformIntegrable f 1 μ) (n : ℕ) :
f n =ᵐ[μ] μ[ℱ.limitProcess f μ|ℱ n] :=
let ⟨_, hR⟩ := hbdd.2.2
hf.eq_condExp_of_tendsto_eLpNorm ((memLp_limitProcess_of_eLpNorm_bdd hbdd.1 hR).integrable le_rfl)
(hf.submartingale.tendsto_eLpNorm_one_limitProcess hbdd) n
