Stability Local Velocity Lp #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_velocity_memLp_three_on_localBox
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
(hsol : IsSuitableWeakSolution Ω I q u Du p 0)
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I Ω' J)
:
MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))
A suitable velocity belongs to L³ on every local box, as required for
the strong limit in thm:stability.