English
If μ is S-finite and κ is a finite kernel, then for any measurable set s ⊆ α × β, the measure of s under μ ⊗ₘ κ equals the integral over a of κ(a) applied to the a-fiber of s.
Русский
Если μ конечна или S-финитна, а κ — конечное ядро, тогда для любого измеримого множества s ⊆ α × β мера μ ⊗ₘ κ на s равна интегралу по a от κ(a) применённой к сечению s на a: s_a = { b : (a,b) ∈ s }.
LaTeX
$$$\\forall {\\alpha} {\\beta}, {m_\\alpha} {m_\\beta}, (μ : \\mathrm{Measure}\\; \\alpha), (κ : \\text{Kernel } \\alpha \\beta), [\\mathrm{SFinite}\\; μ] [\\mathrm{IsSFiniteKernel}\\; κ], {s : \\mathrm{Set}(\\alpha \\times \\beta)}, \\; \\mathrm{MeasurableSet}\\; s \\Rightarrow (μ \\otimes_m κ)\\, s = \\int^- a, κ a (\\mathrm{Prod.mk} \\, a^{-1}' s) \\partial μ$$$
Lean4
theorem compProd_apply [SFinite μ] [IsSFiniteKernel κ] {s : Set (α × β)} (hs : MeasurableSet s) :
(μ ⊗ₘ κ) s = ∫⁻ a, κ a (Prod.mk a ⁻¹' s) ∂μ := by
simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
