Stability Local Finite

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_localBox_finiteMeasure {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

A local box in def:sws has finite space-time measure.