Squared Gaussian cutoff operator bound

The pointwise weak heat inequality has a quadratic form suited to the Gaussian Carleman integral.

theorem ESS.ucGaussianCutoff_operator_sq_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) ^ 2 ≤ 54 * (c₁ * scale) ^ 2 * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v z) ^ 2 + CKN.spatialGradientSq (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv) z) + 3 * (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) ^ 2 + 3 * ((if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)) ^ 2

The squared weak heat operator separates an absorbable cutoff energy from quadratic collar and initial time errors.