stronglyMeasurable_condExp — Mathlib

English

If f =ᵐ[μ] g, then μ[f|m] =ᵐ[μ] μ[g|m].

Русский

Если f =ᵐ[μ] g, тогда μ[f|m] =ᵐ[μ] μ[g|m].

LaTeX

$$$$\\mu[f|m] =_{\\text{ae}} \\mu[g|m].$$$$

Lean4

theorem stronglyMeasurable_condExp : StronglyMeasurable[m] (μ[f|m]) :=
  by
  by_cases hm : m ≤ m₀
  swap; · rw [condExp_of_not_le hm]; exact stronglyMeasurable_zero
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · rw [condExp_of_not_sigmaFinite hm hμm]; exact stronglyMeasurable_zero
  rw [condExp_of_sigmaFinite hm]
  split_ifs with hfi hfm
  · exact hfm
  · exact aestronglyMeasurable_condExpL1.stronglyMeasurable_mk
  · exact stronglyMeasurable_zero

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