condExpKernel_ae — Mathlib

English

For measurable s, the a.e. equality between condExpKernel ω-realisation on s and condExp (restriction) holds after identifying with the left inf of m and mΩ.

Русский

Для измеримого s выполняется a.e. равенство condExpKernel(ω).real s и condExp(м, μ, s.indicator) после идентификации через наименьшее(m, mΩ).

LaTeX

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

Lean4

theorem _root_.MeasureTheory.Integrable.condExpKernel_ae (hf_int : Integrable f μ) :
    ∀ᵐ ω ∂μ, Integrable f (condExpKernel μ m ω) := by
  nontriviality Ω
  rw [condExpKernel_eq]
  convert
    Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using
    1

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