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