English
Let κ: α → β and η: α × β → γ with η finite. Then for a measurable f: β × γ → ℝ≥0∞ and t ⊆ γ measurable, the integral over univ ×ˢ t with respect to (κ ⊗ η) a equals the iterated integral over γ with t on the inner part and κ(a) on the outer part.
Русский
Пусть κ: α → β, η: α × β → γ, η конечно; для измеримого f: β × γ → ℝ≥0∞ и измеримого t ⊆ γ имеем интеграл по univ × t равный двойному интегралу по t и затем по β.
LaTeX
$$$$\\displaystyle \\int^\\!- z \\;\\text{in } \\mathrm{Set.univ} \\timesˢ t\\; f(z) \\; d(κ ⊗ₖ η) a \\\\ = \\int^\\!- x \\; \\int^\\!- y \\; f(x,y) \\; dη(a,x) \\; dκ a,$$$$
Lean4
theorem setLIntegral_compProd_univ_left (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η]
(a : α) {f : β × γ → ℝ≥0∞} (hf : Measurable f) {t : Set γ} (ht : MeasurableSet t) :
∫⁻ z in Set.univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ x, ∫⁻ y in t, f (x, y) ∂η (a, x) ∂κ a := by
simp_rw [setLIntegral_compProd κ η a hf MeasurableSet.univ ht, Measure.restrict_univ]
