tendsto_rpow_atTop — Mathlib

English

For any y > 0, x^y grows slower than exp x; hence exp x / x^y → ∞ as x → ∞.

Русский

Для любого y > 0 экспонента растёт быстрее степенной функции; поэтому exp x / x^y → ∞ при x → ∞.

LaTeX

$$$\text{Tendsto}\bigl( e^{x} / x^{y} \bigr)_{x \to \infty} = \infty \quad (y>0).$$$

Lean4

/-- The function `x ^ y` tends to `+∞` at `+∞` for any positive real `y`. -/
theorem tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ => x ^ y) atTop atTop :=
  by
  rw [(atTop_basis' 0).tendsto_right_iff]
  intro b hb
  filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx
  simpa (disch := positivity) [Real.rpow_inv_le_iff_of_pos] using hx

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