condExp_ae_eq_condExpL1 — Mathlib

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

Похожие утверждения