English
Let f: α → β be measurable and κ: Kernel α γ with IsSFiniteKernel κ. For any a ∈ α and any Measurable g: (β × γ) → ℝ≥0∞, the lintegral over the product of a deterministic kernel at a and κ equals the lintegral of g evaluated at (f(a), ·) with respect to κ a.
Русский
Пусть f: α → β измеримо и κ: Kernel α γ таково, что κ является s-финитным. Для каждого a ∈ α и любого измеримого g: (β × γ) → ℝ≥0∞ имеет место равенство, связывающее линтеграл детерминированного ядра и κ.
LaTeX
$$$\\displaystyle \\int^{\\! -}_{p} g(p) \\, d((\\deterministic f hf) \\times_K \\kappa)(a) \\\\= \\int^{\\! -}_{c} g(f(a), c) \\, d\\kappa(a)(c)$$$
Lean4
theorem lintegral_deterministic_prod {f : α → β} (hf : Measurable f) (κ : Kernel α γ) [IsSFiniteKernel κ] (a : α)
{g : (β × γ) → ℝ≥0∞} (hg : Measurable g) : ∫⁻ p, g p ∂((deterministic f hf) ×ₖ κ) a = ∫⁻ c, g (f a, c) ∂κ a := by
rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']
