Geometry of the Gaussian target box

The target box in lem:uc-gaussian is contained in the plateau of the Carleman cutoff after parabolic dilation.

theorem ESS.uc_gaussian_weight_lower_on_target (a : ℝ) (ha : 0 ≤ a) (center : CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1)) : Real.exp (-(CKN.Foundation.Parabolic.vec3EuclideanNorm center ^ 2 + 1)) ≤ ucGaussianWeight a z

On the normalized target box the Gaussian weight has the lower bound used to return to the unweighted field (lem:uc-gaussian).

theorem ESS.uc_target_box_subset_inner (x₀ x : CKN.Foundation.Parabolic.Vec3) (scale ρ : ℝ) (hscale : 0 < scale) (hρ : 4 ≤ ρ) (hρdef : ρ = 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm ((√(2 / 100))⁻¹ • (x - x₀)) / scale) : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1) ⊆ ucInnerRegion ρ

The normalized target box lies in the interior region of the Gaussian cutoff (lem:uc-gaussian).