tendsto_exp_mul_div_rpow_atTop — Mathlib

English

Let s be any real number and b > 0. Then the function x ↦ e^{b x} / x^{s} tends to +∞ as x → +∞.

Русский

Пусть s — произвольное действительное число, b > 0. Тогда функция x ↦ e^{b x} / x^{s} стремится к +∞ при x → +∞.

LaTeX

$$$$\displaystyle \lim_{x \to +\infty} \frac{e^{b x}}{x^{s}} = +\infty\quad (s \in \mathbb{R},\ b>0).$$$$

Lean4

/-- The function `exp (b * x) / x ^ s` tends to `+∞` at `+∞`, for any real `s` and `b > 0`. -/
theorem tendsto_exp_mul_div_rpow_atTop (s : ℝ) (b : ℝ) (hb : 0 < b) :
    Tendsto (fun x : ℝ => exp (b * x) / x ^ s) atTop atTop :=
  by
  refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_
  filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀
  simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul, mul_comm x, hb.ne', *]

Похожие утверждения