English
The integral over the product kernel equals the iterated integral over η(a,x) and κ a for integrable f.
Русский
Интеграл по произведённому ядру равен повторному интегралу по η и κ для интегрируемой f.
LaTeX
$$$\\int z f(z) \, d(κ \\otimes_k η)a = \\int x \\int y f(x,y) \, dη(a,x) \, dκ a$$$
Lean4
theorem integral_compProd :
∀ {f : β × γ → E} (_ : Integrable f ((κ ⊗ₖ η) a)), ∫ z, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a :=
by
by_cases hE : CompleteSpace E; swap
· simp [integral, hE]
apply Integrable.induction
· intro c s hs h2s
simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
integral_indicator (measurable_prodMk_left hs), MeasureTheory.setIntegral_const, integral_smul_const,
measureReal_def]
congr 1
rw [integral_toReal]
rotate_left
· exact (Kernel.measurable_kernel_prodMk_left' hs _).aemeasurable
· exact ae_kernel_lt_top a h2s.ne
rw [Kernel.compProd_apply hs]
· intro f g _ i_f i_g hf hg
simp_rw [integral_add' i_f i_g, Kernel.integral_integral_add' i_f i_g, hf, hg]
· exact isClosed_eq continuous_integral Kernel.continuous_integral_integral
· intro f g hfg _ hf
convert hf using 1
· exact integral_congr_ae hfg.symm
· apply integral_congr_ae
filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
