lintegral_kernel_prod_left' — Mathlib

English

Let κ be an IsSFiniteKernel. For f : β → α → ENNReal with Measurable (uncurry f), the map y ↦ ∫⁻ x, f(x,y) dκ y is measurable.

Русский

Пусть κ — IsSFiniteKernel. Для f : β → α → ENNReal с измеримостью (uncurry f) отображение y ↦ ∫⁻ x f(x,y) dκ y измеримо.

LaTeX

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

Lean4

@[fun_prop]
theorem _root_.Measurable.lintegral_kernel_prod_left' {f : β × α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun y => ∫⁻ x, f (x, y) ∂κ y := by fun_prop

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