Spatial restriction of weak derivatives

The weak derivative identities remain valid on an open spatial subdomain because every test function there is also a test function on the larger cylinder.

theorem ESS.bu_weak_restrict_space {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} (Set.Ioo 0 1) w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs B (Set.Ioo 0 1) w Dw D2w Dtw

Space-time weak derivatives restrict from the positive half-space to an open spatial subset at the same time interval.