Quadratic control of the normal phase

On the short normalized time interval, the normal Carleman phase has at most three-halves growth in height and is absorbed by a Gaussian.

theorem ESS.bu_short_F_le_three_halves (y s : ℝ) (hy : 0 ≤ y) (hs : s ∈ Set.Ioo (1 / 2) 1) : buShortF y s ≤ y ^ (3 / 2)

The normal phase is at most the three-halves power of height for normalized times between one half and one (lem:bu-small-time).

theorem ESS.bu_short_F_subquadratic_bound (a b : ℝ) (ha : 0 ≤ a) (hb : 0 < b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y s : ℝ), 0 ≤ y → s ∈ Set.Ioo (1 / 2) 1 → 2 * a * buShortF y s ≤ b * y ^ 2 / 2 + C

A fixed normal phase factor is bounded by an arbitrarily small quadratic term plus a constant.