condExpKernel_ae_eq_condExp — Mathlib

English

For hm ≤ mΩ and hs measurable, (condExpKernel μ m ω).real s equals μ⟦s|mⱼΩ for a.e. ω.

Русский

Для hm ≤ mΩ и hs измеримого, condExpKernel μ m ω.real s = μ⟦s|m⟧ a.e.

LaTeX

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

Lean4

theorem condExpKernel_ae_eq_condExp (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun ω ↦ (condExpKernel μ m ω).real s) =ᵐ[μ] μ⟦s|m⟧ :=
  (condExpKernel_ae_eq_condExp' hs).trans (by rw [inf_of_le_left hm])

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