Weak derivatives after compact zero extension

A compactly supported field with globally square-integrable derivative data inherits its weak identities on every larger cylinder containing that data.

theorem ESS.bu_weak_extend_compact {Ω Ω' : Set CKN.Foundation.Parabolic.Vec3} {I I' : Set ℝ} {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hΩ : IsOpen Ω) (hI : IsOpen I) (hKcompact : IsCompact K) (hKsource : K ⊆ CKN.spaceTimeSet Ω I) (hKtarget : K ⊆ CKN.spaceTimeSet Ω' I') (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) (hzero : ∀ z ∉ K, w z = 0 ∧ Dw z = 0 ∧ D2w z = 0 ∧ Dtw z = 0) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (hmem : MeasureTheory.MemLp w 2 MeasureTheory.volume ∧ MeasureTheory.MemLp Dw 2 MeasureTheory.volume ∧ MeasureTheory.MemLp D2w 2 MeasureTheory.volume ∧ MeasureTheory.MemLp Dtw 2 MeasureTheory.volume) : CKN.HasSpaceTimeWeakDerivs Ω' I' w Dw D2w Dtw

Compactly supported weak derivative data extend from a source cylinder to a target cylinder containing their support.