Stability Local Gradient Lp #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_gradient_memLp_two_on_localBox
{Ω Ω' : Set Foundation.Parabolic.Vec3}
{I J : 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)
(hbox : localBox Ω I Ω' J)
:
MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))
The gradient of a suitable solution is square integrable on each local box, as required when passing the weak-gradient term to the limit.