Gaussian weight away from initial time

The Gaussian Carleman weight is uniformly bounded on every positive-time truncation of the normalized cylinder.

theorem ESS.ucGaussianWeight_nonneg (a : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : 0 < z.2) : 0 ≤ ucGaussianWeight a z

The Gaussian weight is nonnegative on positive time.

theorem ESS.ucGaussianWeight_le_after {ε a : ℝ} (hε : 0 < ε) (ha : 0 ≤ a) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hslo : ε ≤ z.2) (hshi : z.2 ≤ 2) : ucGaussianWeight a z ≤ (ε * Real.exp (-(1 / 3))) ^ (-2 * a)

For a fixed positive initial cutoff time, the Gaussian weight has a bound independent of the spatial point.

theorem ESS.ucGaussianWeight_measurable (a : ℝ) : Measurable (ucGaussianWeight a)

The Gaussian weight is measurable on space-time.