English
If f is integrable on the product kernel, then the integral over the product equals the iterated integral of f over η and κ, i.e., ∫ f d(κ ⊗ η) a = ∫x ∫y f(x,y) dη(a,x) dκ(a).
Русский
Если f интегрируема на произведённом ядре, то интеграл по произведению равен повторному интегралу: ∫ f d(κ ⊗ η) a = ∫x ∫y f(x,y) dη(a,x) dκ(a).
LaTeX
$$$\\int z\, f(z)\, d(κ \\otimes_k η)a = \\int x \\int y\, f(x,y) \\, dη(a,x) \\, dκ a$$$
Lean4
theorem _root_.MeasureTheory.Integrable.integral_compProd [NormedSpace ℝ E] ⦃f : β × γ → E⦄
(hf : Integrable f ((κ ⊗ₖ η) a)) : Integrable (fun x => ∫ y, f (x, y) ∂η (a, x)) (κ a) :=
Integrable.mono hf.integral_norm_compProd hf.aestronglyMeasurable.integral_kernel_compProd <|
Eventually.of_forall fun x =>
(norm_integral_le_integral_norm _).trans_eq <|
(norm_of_nonneg <| integral_nonneg_of_ae <| Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm
