Gradient comparison for Gaussian cutoff absorption

A finite dimensional estimate compares the original gradient after multiplication by the cutoff with the weak gradient of the cut off field.

theorem ESS.ucGaussianCutoff_gradient_absorption {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (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} (hz : z ∈ ucCylinder ρ) : ucGaussianCutoff ρ hρ ε z * √(CKN.spatialGradientSq v Dv z) ≤ 3 * (√(CKN.spatialGradientSq (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv) z) + (if z ∈ ucCutoffRegion ρ then CKN.cutoffGradientConstant / ρ else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z))

The gradient of a compact cutoff controls the cutoff factor times the original gradient, with a correction supported on the collar.