setLIntegral_kernel — Mathlib

English

For f : β → α → ENNReal with Measurable (uncurry f) and measurable s ⊆ β, the map b ↦ ∫⁻ a in s, f(a,b) dκ b is measurable.

Русский

Для f : β → α → ENNReal с измеримостью (uncurry f) и измеримого s ⊆ β отображение b ↦ ∫⁻ a in s f(a,b) dκ b измеримо.

LaTeX

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

Lean4

theorem _root_.Measurable.setLIntegral_kernel {f : β → ℝ≥0∞} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
    Measurable fun a => ∫⁻ b in s, f b ∂κ a :=
  Measurable.setLIntegral_kernel_prod_right (by fun_prop) hs

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