English
A version of integral over product kernels restricted to measurable sets in β and γ, with equality to iterated restricted integrals.
Русский
Версия интеграла по произведённому ядру, ограниченная измеримыми множествами, эквивалентна повторному интегралу с ограничениями.
LaTeX
$$$\int z \; d(κ \otimes_k η)a|_{s×t} = ∫ x∈s ∫ y∈t f(x,y) dη(a,x) dκ a$$$
Lean4
theorem setIntegral_compProd {f : β × γ → E} {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
(hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)) :
∫ z in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ x in s, ∫ y in t, f (x, y) ∂η (a, x) ∂κ a := by
-- Porting note: `compProd_restrict` needed some explicit arguments
rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, integral_compProd]
· simp_rw [Kernel.restrict_apply]
· rw [compProd_restrict, Kernel.restrict_apply]; exact hf
