condExpKernel_ae_eq_trim_condExp — Mathlib

English

On μ.trim hm, the a.e. equality of condExpKernel ω-real s with condExp mΩ holds for measurable s.

Русский

На μ.trim hm a.e. condExpKernel ω.real s равен condExp mΩ для измеримого s.

LaTeX

$$$(condExpKernel_{\\mu,m})_{\\omega}.real(s) =^a.e_{μ.trim hm} μ⟦s|mΩ⟧$$$

Lean4

theorem condExpKernel_ae_eq_trim_condExp (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun ω ↦ (condExpKernel μ m ω).real s) =ᵐ[μ.trim hm] μ⟦s|m⟧ :=
  by
  simp_rw [measureReal_def]
  rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm stronglyMeasurable_condExp]
  exact condExpKernel_ae_eq_condExp hm hs

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