integral_condExpKernel — Mathlib

English

If f is integrable, then ω ↦ ∫ f d condExpKernel μ m ω is integrable (as a function of ω).

Русский

Если f интегрируема, то ω ↦ ∫ f d condExpKernel μ m ω интегрируема по ω.

LaTeX

$$$\\text{Integrable}_{μ}(\\,f)\\Rightarrow \\text{Integrable}_{μ}(\\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] (fun ω ↦ ∫ y, f y ∂condExpKernel μ m ω) :=
  hf.integral_condExpKernel'.mono inf_le_left

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