Pressure Split Tensor #
Supporting estimates for the Navier–Stokes development.
The unit spatial ball crossed with the negative unit time interval, supporting the pressure-split source.
Equations
Instances For
noncomputable def
CKN.pressureSplitTensor
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(i j : Fin 3)
:
The tensor used by the pressure split, extended by zero outside the unit space-time cylinder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.pressureSplitTensor_memLp
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (k : Fin 3),
HasWeakGradientOn (Foundation.Parabolic.vec3Ball 0 1) (fun (x : Vec 3) => u (x, t) k) fun (x : Vec 3) =>
Du (x, t) k)
(i j : Fin 3)
:
MeasureTheory.MemLp (pressureSplitTensor u i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume
The zero-extended tensor has space-time L^(3/2) under the local
energy, L^infinity_t L^3_x, and weak-gradient hypotheses.