integral_condExpKernel — Mathlib

English

If f is AEStronglyMeasurable, then the ω-average of the integral ∫ f d condExpKernel μ m ω is AEStronglyMeasurable.

Русский

Если f — AEStronglyMeasurable, то среднее по ω от интеграла ∫ f d condExpKernel μ m ω является AEStronglyMeasurable.

LaTeX

$$$\\text{AEStronglyMeasurable}(f)\\Rightarrow \\text{AEStronglyMeasurable}_{μ}(\\omega\\mapsto \\int y\\; f(y)\\; d condExpKernel(\\mu,m)(\\omega))$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condExpKernel [NormedSpace ℝ F]
    (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ :=
  by
  nontriviality Ω
  simp_rw [condExpKernel_apply_eq_condDistrib]
  exact
    AEStronglyMeasurable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      (hf.comp_snd_map_prod_id inf_le_right)

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