Polynomial control of Gaussian decay

An exponential with negative reciprocal time is bounded by any fixed positive integer power of time.

theorem ESS.uc_exp_neg_div_le_pow (b t : ℝ) (n : ℕ) (hb : 0 < b) (ht : 0 < t) (hn : 0 < n) : Real.exp (-(b / t)) ≤ (↑n * t / b) ^ n

A reciprocal-time Gaussian is bounded by an explicit polynomial.