Gaussian weight on the cutoff collar

The weight in lem:uc-gaussian is exponentially small where the spatial or final-time cutoff changes.

theorem ESS.uc_log_weight_three_half_bounds : 1 / 5 ≤ Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)) ∧ Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)) ≤ 2 / 3

Numerical bounds for the time weight at the Gaussian cutoff threshold (eq:uc-collar-weight).

theorem ESS.uc_gaussian_collar_weight (ρ : ℝ) (hρ : 4 ≤ ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ ucCutoffRegion ρ) : ucGaussianWeight (1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)))) z ≤ Real.exp (-ρ ^ 2 / 100)

The Gaussian weight is exponentially small on the spatial and final-time collar (eq:uc-collar-weight).