norm_integral_condExpKernel — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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