Is Locally Square Integrable Force #
Supporting estimates for the Navier–Stokes development.
def
CKN.IsLocallySquareIntegrableForce
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Square integrability of the force on every finite positive-time slab.
Equations
- CKN.IsLocallySquareIntegrableForce f = ∀ (T : ℝ), 0 < T → MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))