Gradient of a scalar cutoff field

The weak product gradient controls the cutoff factor times the original gradient, with an explicit term for derivatives of the scalar cutoff.

theorem ESS.buCut_gradient_absorption (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hκ : 0 ≤ buCutScalar κ z) (M : ℝ) (hM : 0 ≤ M) (hderiv : ∀ (j : Fin 3), |CKN.spatialPartial (buCutScalar κ) j z| ≤ M) : buCutScalar κ z * √(CKN.spatialGradientSq v Dv z) ≤ 3 * (√(CKN.spatialGradientSq (buCutField κ v) (buCutDw κ v Dv) z) + M * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z))

A pointwise gradient comparison for the scalar cutoff used in lem:bu-small-time.