Geometry of the Gaussian rescaling

The translated parabolic cylinder used in lem:uc-gaussian stays inside the source cylinder.

theorem ESS.uc_gaussian_scale_geometry (R T γ t : ℝ) (hT : 0 < T) (hγ' : γ < 3 / 16) (x₀ x : CKN.Foundation.Parabolic.Vec3) (ht : 0 < t) (ht' : t ≤ γ * T) (hx : CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 3 / 8 * √(2 / 100) * R) (hd : 16 / 100 * t ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ^ 2) : have scale := √(2 * t); have X := (√(2 / 100))⁻¹ • (x - x₀); have ρ := 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm X / scale; 4 ≤ ρ ∧ scale * ρ ≤ 3 * R / 4 ∧ 2 * scale ^ 2 ≤ 3 * T / 4

The output-point conditions of lem:uc-gaussian give the scaled radius and the source-cylinder inclusion inequalities.