Restricting weak derivatives to a shorter time interval

The time changes in lem:bu-iterate and thm:bu use weak derivatives on subintervals of the positive-time cylinder.

theorem ESS.bu_weak_restrict_time {I : Set ℝ} (hI : I ⊆ Set.Ioo 0 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} I w Dw D2w Dtw

Space-time weak derivatives restrict to a shorter time interval in the same positive half-space.