English
If b > 0, then (b e^x + c)/x^n tends to +∞ as x → +∞ for any n.
Русский
Если b > 0, то (b e^x + c)/x^n стремится к +∞ при x → +∞ для любого n.
LaTeX
$$$\\text{If } b>0:\\; \\lim_{x\\to +\\infty} \\frac{b e^{x} + c}{x^{n}} = +\\infty \\quad (n\\in\\mathbb{N}).$$$
Lean4
/-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any natural number
`n` and any real numbers `b` and `c` such that `b` is positive. -/
theorem tendsto_mul_exp_add_div_pow_atTop (b c : ℝ) (n : ℕ) (hb : 0 < b) :
Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop :=
by
rcases eq_or_ne n 0 with (rfl | hn)
· simp only [pow_zero, div_one]
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds
simp only [add_div, mul_div_assoc]
exact
((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))
