Exponential normal-phase bound

At fixed Carleman parameter, the normal phase exponential is bounded by an arbitrarily weak quadratic exponential times a constant.

theorem ESS.bu_short_normal_phase_exp_le_quadratic (scale a b : ℝ) (ha : 0 ≤ a) (hb : 0 < b) : ∃ (C : ℝ), 0 < C ∧ ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ z.1 2 → z.2 ∈ Set.Ioo (1 / 2) 1 → Real.exp (2 * a * (buShortF (z.1 2) z.2 - buShortB scale)) ≤ C * Real.exp (b * z.1 2 ^ 2)

A fixed shifted normal phase is dominated by a quadratic Gaussian exponent on the short-time slab (lem:bu-small-time).