Exponential decay at the initial time

Gaussian decay dominates every inverse power of time, as used in lem:uc-gaussian and thm:uc.

theorem ESS.uc_exp_dominates_inverse_power (b p : ℝ) (hb : 0 < b) : Filter.Tendsto (fun (t : ℝ) => t.rpow (-p) * Real.exp (-(b / t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A positive Gaussian exponent dominates any inverse power as time tends to zero from above.