Stability Local Product Integral

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_setIntegral_localBox_eq_prod {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (F : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, F z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F (z.1, z.2) ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)

A local-box scalar integral in CKN coordinates equals its ordinary product-measure integral.