integral_condExpKernel' — Mathlib

English

If f is strongly measurable, then the map ω ↦ ∫ y f(y) d condExpKernel μ m ω is strongly measurable.

Русский

Если f сильно измерима, тогда отображение ω ↦ ∫ y f(y) d condExpKernel μ m ω является сильно измеримой функцией.

LaTeX

$$$\\mathrm{StronglyMeasurable}(\\omega\\mapsto \\int y\\; f(y)\\; d condExpKernel(\\mu,m)(\\omega))$$$

Lean4

theorem _root_.MeasureTheory.StronglyMeasurable.integral_condExpKernel' [NormedSpace ℝ F] (hf : StronglyMeasurable f) :
    StronglyMeasurable[m ⊓ mΩ] (fun ω ↦ ∫ y, f y ∂condExpKernel μ m ω) :=
  by
  nontriviality Ω
  simp_rw [condExpKernel_apply_eq_condDistrib]
  exact (hf.comp_measurable measurable_snd).integral_condDistrib

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