Gaussian cutoff operator bound

The normalized heat inequality and the weak product rule separate an absorbable term from collar and initial time errors.

theorem ESS.ucGaussianCutoff_operator_ae_bound {ρ ε c₁ scale : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hc₁ : 0 ≤ c₁) (hscale : 0 ≤ scale) (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) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), z ∈ ucCylinder ρ → CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z) ≤ (c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v z) + 3 * √(CKN.spatialGradientSq (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv) z)) + if z ∈ ucCutoffRegion ρ then (32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) + 3 * c₁ * scale * (CKN.cutoffGradientConstant / ρ)) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * (CKN.cutoffGradientConstant / ρ) * √(CKN.spatialGradientSq v Dv z) else 0) + (if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)

The cut off heat operator is controlled by the cut off field and its weak gradient, with errors confined to the collar and early time.