English
For integrable f: α×β → E, the double integral equals the iterated integral with the order of integration reversed.
Русский
Для интегрируемой функции f: α×β → E двойной интеграл равен итерационному интегралу с обратным порядком интегрирования.
LaTeX
$$$$\\int_{α×β} f(x,y) \\, dμ×ν = \\int_{β} \\left( \\int_{α} f(x,y) \\, dμ(x) \\right) dν(y).$$$$
Lean4
/-- Symmetric version of **Fubini's Theorem**: For integrable functions on `α × β`,
the Bochner integral of `f` is equal to the iterated Bochner integral.
This version has the integrals on the right-hand side in the other order. -/
theorem integral_prod_symm (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
∫ z, f z ∂μ.prod ν = ∫ y, ∫ x, f (x, y) ∂μ ∂ν := by rw [← integral_prod_swap f]; exact integral_prod _ hf.swap
