Is Locally QIntegrable Force #
Supporting estimates for the Navier–Stokes development.
def
CKN.IsLocallyQIntegrableForce
(q : ℝ)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Local L^q integrability of the force on the cylinders in def:sws.
Equations
- CKN.IsLocallyQIntegrableForce q f = ∀ (Ω' : Set CKN.Foundation.Parabolic.Vec3) (J : Set ℝ), CKN.localBox Set.univ (Set.Ioi 0) Ω' J → CKN.localVecLp (CKN.spaceTimeSet Ω' J) q f