Localized Gaussian cutoff operator bound

The cutoff error is separated into the spatial transition shell, the final time transition, and the initial trace transition (lem:bu-gaussian).

theorem ESS.buGaussian_cutoff_operator_localized_ae_bound {ρ ε c₁ scale : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hεsmall : 2 * ε ≤ 1 / 2) (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.1 ∈ {y : CKN.Foundation.Parabolic.Vec3 | 13 * ρ / 20 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ 3 * ρ / 4} 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 3 / 2 ≤ z.2 ∧ z.2 ≤ 7 / 4 then 32 * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) else 0) + (if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then 8 / ε else 0) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)

The Gaussian cutoff heat operator is bounded separately on the spatial transition shell, the final-time strip, and the initial-time strip (lem:bu-gaussian).