English
Under sigma-finite μ, the conditional expectation equals condExpL1 almost everywhere.
Русский
При сигма-конечной μ условное ожидание равно condExpL1 почти наверху.
LaTeX
$$$$\\mu[f|m] =_{\\text{ae}} condExpL1 hm \\mu f.$$$$
Lean4
theorem condExp_ae_eq_condExpL1 (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] (f : α → E) :
μ[f|m] =ᵐ[μ] condExpL1 hm μ f := by
rw [condExp_of_sigmaFinite hm]
by_cases hfi : Integrable f μ
· rw [if_pos hfi]
by_cases hfm : StronglyMeasurable[m] f
· rw [if_pos hfm]
exact (condExpL1_of_aestronglyMeasurable' hfm.aestronglyMeasurable hfi).symm
· rw [if_neg hfm]
exact aestronglyMeasurable_condExpL1.ae_eq_mk.symm
rw [if_neg hfi, condExpL1_undef hfi]
exact (coeFn_zero _ _ _).symm