Product rules for the space and phase cutoffs

The spatial cutoff and normal-phase cutoff are differentiated before the lower-time factor is added.

theorem ESS.bu_spatialSecondPartial_mul_full {a b : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (hb : ContDiff ℝ (↑⊤) b) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => a q * b q) j j z = CKN.spatialSecondPartial a j j z * b z + 2 * CKN.spatialPartial a j z * CKN.spatialPartial b j z + a z * CKN.spatialSecondPartial b j j z

The diagonal Hessian of a product has the two cross terms of the ordinary product rule.