English
Let κ: α → β and η: α → γ be s-finite kernels. For every a ∈ α and every Measurable g: β × γ → ℝ≥0∞, the integral of g with respect to the product kernel κ ×K η at a equals the iterated integral, first with respect to κ a and then with respect to η a. In symbols: ∫⁻ g d(κ ×ₖ η) a = ∫⁻ c ( ∫⁻ b g(b,c) dκ a ) dη a.
Русский
Пусть κ: α → β и η: α → γ — ядра с конечной S-сходимостью. Для любого a ∈ α и для любых измеримых g: β × γ → ℝ≥0∞ выполняется равенство
LaTeX
$$$\\displaystyle \\int^{\\! -}_{c} g(c) \\, d(\\kappa \\times_K \\eta)(a) \;=\\; \\int^{\\! -}_{c} \\left( \\int^{\\! -}_{b} g(b,c) \\, d\\kappa(a)(b) \\right) \\, d\\eta(a)(c)$$$
Lean4
theorem lintegral_prod_symm (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α)
{g : β × γ → ℝ≥0∞} (hg : Measurable g) : ∫⁻ c, g c ∂(κ ×ₖ η) a = ∫⁻ c, ∫⁻ b, g (b, c) ∂κ a ∂η a := by
rw [prod_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]
