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