setLIntegral_kernel_prod_left — Mathlib

English

For κ : Kernel α β and measurable f : β → ENNReal with Measurable f, the map a ↦ ∫⁻ b, f(b) ∂κ a is measurable.

Русский

Для κ: Kernel α β и измеримого f : β → ENNReal отображение a ↦ ∫⁻ b f(b) ∂κ a измеримо.

LaTeX

$$$\\text{Measurable}\\left( a \\mapsto \\int⁻ b \\; f(b) \\, dκ a\\right)$$$

Lean4

theorem _root_.Measurable.setLIntegral_kernel_prod_left {f : β → α → ℝ≥0∞} (hf : Measurable (uncurry f)) {s : Set β}
    (hs : MeasurableSet s) : Measurable fun b => ∫⁻ a in s, f a b ∂κ b := by simp_rw [← lintegral_restrict κ hs];
  fun_prop

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