integral_condExpKernel — Mathlib

English

If f is integrable, then ω ↦ ∫ f(y) d condExpKernel μ m ω is integrable with respect to μ.

Русский

Если f интегрируема, то функция ω ↦ ∫ f(y) d condExpKernel μ m ω интегрируема по μ.

LaTeX

$$$\\text{Integrable}(f,μ) \\Rightarrow \\text{Integrable}(ω\\mapsto \\int y\\, f(y)\\, d condExpKernel(μ,m)(ω))$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_condExpKernel [NormedSpace ℝ F] (hf_int : Integrable f μ) :
    Integrable (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ :=
  by
  nontriviality Ω
  rw [condExpKernel_eq]
  convert
    Integrable.integral_condDistrib (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

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