Restricting Leray–Hopf solutions to shorter intervals #
A Leray–Hopf solution on (0, T) is one on every shorter interval (0, σ)
with the same datum (def:leray-hopf).
theorem
CKN.IsLerayHopfSolution.restrict
{T σ : ℝ}
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hU : IsLerayHopfSolution T a u Du)
(hσ : 0 < σ)
(hσT : σ ≤ T)
:
IsLerayHopfSolution σ a u Du
Restriction of a Leray–Hopf solution to a shorter time interval.