Polynomial absorption by a Gaussian

A fixed positive quadratic exponential dominates the fourth power of one plus the normal height.

theorem ESS.bu_short_fourth_power_le_exp_sq (b y : ℝ) (hb : 0 < b) : (1 + y) ^ 4 ≤ 8 * (1 + 4 / b ^ 2) * Real.exp (b * y ^ 2)

The fourth-order normal cutoff factor is bounded by a quadratic exponential (lem:bu-small-time).