English
For κ: α → β and η: α × β → γ with η finite, and a fixed a ∈ α, for a measurable f: β × γ → ℝ≥0∞, the L¹-like integral over s × univ with respect to (κ ⊗η) a equals the iterated integral over s and then over γ with η(a, x) and κ(a).
Русский
Пусть κ: α → β, η: α × β → γ, η конечное; для фиксированного a ∈ α и измеримого f: β × γ → ℝ≥0∞ имеем аналогичный разложимый интеграл по s × univ.
LaTeX
$$$$\\displaystyle \\int^{\\infty}_{z \\in s \\timesˢ Set.univ} f(z)\\, d(κ ⊗ₖ η) a \\\\ = \\int^{\\infty}_{x \\in s} \\Big( \\int^{\\infty}_{y} f(x,y) \\; dη(a,x) \\Big) dκ a,$$$$
Lean4
theorem setLIntegral_compProd_univ_right (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η]
(a : α) {f : β × γ → ℝ≥0∞} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
∫⁻ z in s ×ˢ Set.univ, f z ∂(κ ⊗ₖ η) a = ∫⁻ x in s, ∫⁻ y, f (x, y) ∂η (a, x) ∂κ a := by
simp_rw [setLIntegral_compProd κ η a hf hs MeasurableSet.univ, Measure.restrict_univ]
