Limits of P(x) / e ^ x for a polynomial P

In this file we prove that $\lim_{x\to\infty}\frac{P(x)}{e^x}=0$ for any polynomial P.

TODO

Add more similar lemmas: limit at -∞, versions with $e^{cx}$ etc.

Keywords

polynomial, limit, exponential

theorem Polynomial.tendsto_div_exp_atTop (p : Polynomial ℝ) : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x p / Real.exp x) Filter.atTop (nhds 0)