Spatial restriction on translated time intervals

The weak derivative identities remain valid on an open spatial subdomain on the corresponding cylinder, including after the initial-time shift.

theorem ESS.bu_weak_restrict_space_interval {I : Set ℝ} (hI : MeasurableSet I) {B : Set CKN.Foundation.Parabolic.Vec3} (hB : B ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}) (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} I w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs B I w Dw D2w Dtw

Space-time weak derivatives restrict from the positive half-space to a spatial subset at any measurable time interval.