Restricting finite-energy weak solutions to shorter intervals

A finite-energy weak solution with pressure on (0, T) is one on every shorter interval (0, σ). The short-time comparison in thm:ess-l5-unique applies lem:pv-serrin-uniqueness on such an interval.

theorem ESS.IsSerrinWeakSolution.restrict {T σ : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du p) (hσ : 0 < σ) (hσT : σ ≤ T) : IsSerrinWeakSolution σ a u Du p

Restriction of a finite-energy weak solution with pressure to a shorter time interval.