setLIntegral_kernel_prod_right — Mathlib

English

For f : β × α → ENNReal, if f is measurable, then a function y ↦ ∫⁻ x, f(x,y) dκ y is measurable.

Русский

Для f : β × α → ENNReal измерима тогда, когда y ↦ ∫⁻ x f(x,y) dκ y измерима.

LaTeX

$$$\\text{Measurable}\\bigl(y \\mapsto \\int⁻ x\\, f(x,y) \\, d\\kappa y\\bigr)$$$

Lean4

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

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