Geometry of the Gaussian average rescaling

The translated parabolic coordinates in lem:bu-gaussian remain in the positive half-space and below time one.

def ESS.buGaussianScaledPoint (x : CKN.Foundation.Parabolic.Vec3) (scale σ : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.ParabolicPoint

The translated parabolic point used in lem:bu-gaussian.

Equations

• ESS.buGaussianScaledPoint x scale σ z = (x + scale • z.1, scale ^ 2 * (z.2 - σ))

theorem ESS.buGaussian_rescaling_geometry (x : CKN.Foundation.Parabolic.Vec3) (t γ : ℝ) (ht : 0 < t) (hγ : γ ≤ 1 / 12) (htγ : t < γ) : have scale := √(3 * t); have ρ := (x 2 - 1) / scale; 0 < scale ∧ scale < 1 ∧ (∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm y < ρ → 1 < (x + scale • y) 2) ∧ ∀ (s : ℝ), 1 / 6 < s → s < 3 → 0 < scale ^ 2 * (s - 1 / 6) ∧ scale ^ 2 * (s - 1 / 6) < 1

The normalized cylinder maps into the original positive half-space and time interval of lem:bu-gaussian.

theorem ESS.buGaussian_rescaling_growth (A scale : ℝ) (x y : CKN.Foundation.Parabolic.Vec3) (s σ : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hA : 0 ≤ A) (hscale : 0 ≤ scale) (hgrowth : CKN.Foundation.Parabolic.vec3EuclideanNorm (w (buGaussianScaledPoint x scale σ (y, s))) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianScaledPoint x scale σ (y, s)).1 ^ 2)) : CKN.Foundation.Parabolic.vec3EuclideanNorm (w (buGaussianScaledPoint x scale σ (y, s))) ≤ Real.exp (2 * A * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 + 2 * A * scale ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm y ^ 2)

The squared growth bound after the Gaussian rescaling has its source form.