Cutoff data outside the scalar support

Every specified weak derivative of the cutoff field vanishes off the closed support of its smooth scalar factor.

theorem ESS.buCut_data_zero_off_support (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∉ buCutSupportSet κ) : buCutField κ v z = 0 ∧ buCutDw κ v Dv z = 0 ∧ buCutD2 κ v Dv D2v z = 0 ∧ buCutDt κ v Dtv z = 0

The cutoff field and all its specified weak derivative data vanish outside the topological support of the scalar cutoff.