English
Let κ be a finite kernel from α to β and η a finite kernel from α × β to γ. For any fixed a ∈ α and any measurable nonnegative function f: β × γ → ℝ≥0∞, the integral of f over the set s × t with respect to the product kernel κ ⊗η at a equals the iterated integral: integrate over s in β and then over t in γ with η(a, x) and κ(a) respectively.
Русский
Пусть κ — конечное ядро из α в β, η — конечное ядро из α × β в γ. Пусть a ∈ α и f: β × γ → ℝ≥0∞ измеримо. Тогда интеграл по множеству s × t относительно произведения ядер κ ⊗ η на a равен повторному интегралу: по x из s затем по y из t с использованием η(a, x) и κ(a).
LaTeX
$$$\\displaystyle \\int^\\! - z \\;\\text{in } s \\timesˢ t\\; f(z) \\\\ d(\\kappa \\otimes_{\\kern-0.2em η) a} \\\\ = \\,\\int^\\! - x \\;\\text{in } s\\; \\Big( \\int^\\! - y \\; \\text{in } t\\; f(x,y) \\, dη(a,x) \\, dκ(a) \\Big)$$$
Lean4
theorem setLIntegral_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
{f : β × γ → ℝ≥0∞} (hf : Measurable f) {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
∫⁻ z in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ x in s, ∫⁻ y in t, f (x, y) ∂η (a, x) ∂κ a := by
simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, lintegral_compProd _ _ _ hf,
Kernel.restrict_apply]
