Spatial localization for Gaussian average cutoffs

The spatial cutoff is constant on a larger inner ball and vanishes outside its compact support. These regions localize the two collar errors in lem:bu-gaussian.

theorem ESS.buGaussian_spatial_cutoff_eq_one_on_plateau {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 (13 * ρ / 20)) : ucSpatialCutoff ρ hρ y = 1

The CKN ball cutoff is constant on the inner plateau used for the Gaussian average collar estimate.

theorem ESS.buGaussian_spatial_cutoff_partial_zero_on_plateau {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 (13 * ρ / 20)) (j : Fin 3) (s : ℝ) : CKN.spatialPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ z.1) j (y, s) = 0

The spatial derivative vanishes on the larger Gaussian plateau.

theorem ESS.buGaussian_spatial_cutoff_second_zero_on_plateau {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 (13 * ρ / 20)) (i j : Fin 3) (s : ℝ) : CKN.spatialSecondPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ z.1) i j (y, s) = 0

The spatial Hessian vanishes on the larger Gaussian plateau.

theorem ESS.buGaussian_spatial_cutoff_partial_zero_outside {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : 3 * ρ / 4 < CKN.Foundation.Parabolic.vec3EuclideanNorm y) (j : Fin 3) (s : ℝ) : CKN.spatialPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ z.1) j (y, s) = 0

The spatial derivative of the ball cutoff vanishes outside its support ball.

theorem ESS.buGaussian_spatial_cutoff_second_zero_outside {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : 3 * ρ / 4 < CKN.Foundation.Parabolic.vec3EuclideanNorm y) (i j : Fin 3) (s : ℝ) : CKN.spatialSecondPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ z.1) i j (y, s) = 0

The spatial Hessian of the ball cutoff vanishes outside its support ball.

theorem ESS.buGaussian_cutoff_heat_zero_outside {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : 3 * ρ / 4 < CKN.Foundation.Parabolic.vec3EuclideanNorm z.1) (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) : ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z = 0

The Gaussian cutoff heat operator vanishes outside the spatial support ball, independently of its time cutoffs.

theorem ESS.buGaussian_cutoff_heat_eq_on_plateau_after_initial {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : z.1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 (13 * ρ / 20)) (hεtime : 2 * ε < z.2) (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) : ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv z = ucFinalTimeCutoff z.2 • ucWeakHeatVector D2v Dtv z + deriv ucFinalTimeCutoff z.2 • v z

On the enlarged spatial plateau after the initial transition, the cutoff heat operator has only the final-time cutoff error.