condExp_of_aestronglyMeasurable' — Mathlib

English

For sigma-finite μ and integrable f, μ[f|m] is equal a.e. to condExpL1 hm μ f, and the a.e. equality holds under trimming.

Русский

Для сигма-конечной μ и интегрируемого f, μ[f|m] равен a.e. CondExpL1 hm μ f, и равенство сохраняется под усечением.

LaTeX

$$$$\\mu[f|m] =_{\\text{ae}} condExpL1 hm μ f.$$$$

Lean4

theorem condExp_of_aestronglyMeasurable' (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] {f : α → E}
    (hf : AEStronglyMeasurable[m] f μ) (hfi : Integrable f μ) : μ[f|m] =ᵐ[μ] f :=
  by
  refine ((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm
  rw [condExp_of_stronglyMeasurable hm hf.stronglyMeasurable_mk ((integrable_congr hf.ae_eq_mk).mp hfi)]

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