Restart of the global real mild trajectory

The global regularized mild curve satisfies the same mild equation when viewed from any nonnegative start time.

theorem CKN.Leray.regularizedGlobalMildCurve_shift_isTrajectory (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b₀ : ↥RealVectorL2) (hbJ : RegularizedMildJData b₀) (a T : ℝ) (ha : 0 ≤ a) (hT : 0 ≤ T) : IsRegularizedMildTrajectory ρ ε hε (regularizedGlobalMildCurve ρ ε hε b₀ hbJ a) T (regularizedGlobalMildCurveShiftPath ρ ε hε b₀ hbJ a T)

The global mild curve restricted after a nonnegative start time is a mild trajectory with its state at that time as initial datum.