Exponents under short-time rescaling

The spatial growth exponent scales quadratically, while the normal Gaussian decay retains an inverse dyadic time scale.

theorem ESS.bu_short_vec3_norm_sq_coordinates (Y : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm Y ^ 2 = Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2

The squared Euclidean norm in three coordinates is the sum of the three coordinate squares (lem:bu-small-time).

theorem ESS.bu_short_average_normal_tail_le (scale β δ d : ℝ) (Y : CKN.Foundation.Parabolic.Vec3) (hscale : 0 < scale) (hβ : 0 < β) (hδ : 0 < δ) (hδd : δ ≤ d) : have t := scale ^ 2 * δ / 2; have X := scale • Y; Real.exp (-(β * X 2 ^ 2 / (12 * t))) ≤ Real.exp (-(β * Y 2 ^ 2 / (12 * d)))

The physical Gaussian normal tail dominates the dyadic normal tail after short-time rescaling (lem:bu-small-time).