English
Fubini-type equality for inner integral: ∫ f d(η ∘ₖ κ) = ∫∫ f dη dκ.
Русский
Неравенство Фубини для вложенного интеграла.
LaTeX
$$$$ \\int f\,d(\\eta \\circ κ) = \\int a \\int b f(a,b)\,dκ(a)\,dμ(a) $$$$
Lean4
theorem integral_comp : ∀ {f : γ → E} (_ : Integrable f ((η ∘ₖ κ) a)), ∫ z, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y, f y ∂η x ∂κ a :=
by
by_cases hE : CompleteSpace E; swap
· simp [integral, hE]
apply Integrable.induction
· intro c s hs ms
simp_rw [integral_indicator hs, MeasureTheory.setIntegral_const, integral_smul_const, measureReal_def]
congr
rw [integral_toReal, Kernel.comp_apply' _ _ _ hs]
· exact (Kernel.measurable_coe _ hs).aemeasurable
· exact ae_lt_top_of_comp_ne_top a ms.ne
· rintro f g - i_f i_g hf hg
simp_rw [integral_add' i_f i_g, integral_integral_add'_comp i_f i_g, hf, hg]
· exact isClosed_eq continuous_integral Kernel.continuous_integral_integral_comp
· rintro f g hfg - hf
convert hf using 1
· exact integral_congr_ae hfg.symm
· apply integral_congr_ae
filter_upwards [ae_ae_of_ae_comp hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
