Stability Local Energy

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_local_energy_lintegral_lt_top {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤

Local L³ velocity and L² gradient bounds supply the joint energy integrability in (S1) of def:sws (thm:stability).