Weak product rule for the Gaussian cutoff

Smooth compactly supported factors preserve the weak integration-by-parts identities used in lem:uc-gaussian.

theorem ESS.ucCutoff_hasSpaceTimeWeakDerivs {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (hξ : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ucCutoffScalar θ η χ z) {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} (hw : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs Ω I (ucCutoffField θ η χ w) (ucCutoffDw θ η χ w Dw) (ucCutoffD2 θ η χ w Dw D2w) (ucCutoffDt θ η χ w Dtw)

Smooth scalar multiplication preserves the space-time weak derivative structure, with the usual first, second, and time product rules.