Absorption of the normal phase

A fixed multiple of the three-halves power is bounded above by an arbitrarily small quadratic term plus a constant.

theorem ESS.bu_short_rpow_three_halves_eq_mul_sqrt (y : ℝ) (hy : 0 ≤ y) : y ^ (3 / 2) = y * √y

The three-halves power is the product of height and its square root at nonnegative height.

theorem ESS.bu_short_subquadratic_bound (a b : ℝ) (ha : 0 ≤ a) (hb : 0 < b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), 0 ≤ y → a * y ^ (3 / 2) ≤ b * y ^ 2 / 2 + C

Any fixed normal three-halves phase is absorbed by a positive quadratic Gaussian, up to a finite constant (lem:bu-small-time).