English
Let f: α×β → E be integrable with respect to μ×ν. Then the Bochner integral over μ×ν equals the iterated integral ∫x ∫y f(x,y).
Русский
Пусть f: α×β → E интегрируема по μ×ν. Тогда интеграл по μ×ν равен итерационному интегралу ∫x ∫y f(x,y).
LaTeX
$$$$\\int_{α×β} f(x,y) \\, dμ×ν = \\int_{α} \\left( \\int_{β} f(x,y) \\, dν(y) \\right) dμ(x).$$$$
Lean4
/-- **Fubini's Theorem**: For integrable functions on `α × β`,
the Bochner integral of `f` is equal to the iterated Bochner integral.
`integrable_prod_iff` can be useful to show that the function in question in integrable.
`MeasureTheory.Integrable.integral_prod_right` is useful to show that the inner integral
of the right-hand side is integrable. -/
theorem integral_prod (f : α × β → E) (hf : Integrable f (μ.prod ν)) : ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ :=
by
by_cases hE : CompleteSpace E; swap; · simp only [integral, dif_neg hE]
revert f
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), setIntegral_const, integral_smul_const, measureReal_def,
integral_toReal (measurable_measure_prodMk_left hs).aemeasurable (ae_measure_lt_top hs h2s.ne)]
rw [prod_apply hs]
· rintro f g - i_f i_g hf hg
simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
· exact isClosed_eq continuous_integral continuous_integral_integral
· 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_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
