English
If one inner integral is an interval integral, the order of integration can be swapped, yielding equality of the two iterated expressions.
Русский
Если одна из внутренних интегралов является интегралом по интервалу, можно поменять порядок интегрирования и получить равенство двух выражений.
LaTeX
$$$$\\int_a^b \\int g = \\int g \\; dx.$$$$
Lean4
/-- Change the order of integration, when one of the integrals is an interval integral. -/
theorem intervalIntegral_integral_swap {a b : ℝ} {f : ℝ → α → E}
(h_int : Integrable (uncurry f) ((volume.restrict (Set.uIoc a b)).prod μ)) :
∫ x in a..b, ∫ y, f x y ∂μ = ∫ y, (∫ x in a..b, f x y) ∂μ :=
by
rcases le_total a b with (hab | hab)
· simp_rw [intervalIntegral.integral_of_le hab]
simp only [hab, Set.uIoc_of_le] at h_int
exact integral_integral_swap h_int
· simp_rw [intervalIntegral.integral_of_ge hab]
simp only [hab, Set.uIoc_of_ge] at h_int
rw [integral_integral_swap h_int, integral_neg]
