Prod Swap

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Parabolic.Integration.prod_lintegral_swap_cyl {S : Set Vec3} {T : Set ℝ} {F : Vec3 × ℝ → ENNReal} (hF : AEMeasurable F ((MeasureTheory.volume.restrict S).prod (MeasureTheory.volume.restrict T))) : ∫⁻ (z : Vec3 × ℝ) in S ×ˢ T, F z = ∫⁻ (s : ℝ) in T, ∫⁻ (y : Vec3) in S, F (y, s)

Tonelli's theorem for set integrals on a product of a spatial set S ⊆ Vec3 and a time interval T ⊆ ℝ: the integral of a nonnegative measurable function over the cylinder S ×ˢ T equals the iterated integral with the time variable outermost, using the product Lebesgue measure on Vec3 × ℝ.