Is Global Leray Hopf Solution #
Supporting estimates for the Navier–Stokes development.
def
CKN.IsGlobalLerayHopfSolution
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
:
A global Leray–Hopf solution on every finite interval, as in
rem:global-LH.
Equations
- CKN.IsGlobalLerayHopfSolution a u Du = ∀ (T : ℝ), 0 < T → CKN.IsLerayHopfSolution T a u Du