English
For every natural n, the ratio exp(x)/x^n tends to +∞ as x → +∞.
Русский
Для любого натурального n дробь exp(x)/x^n стремится к +∞ при x → +∞.
LaTeX
$$$\\displaystyle \\lim_{x \\to +\\infty} \\frac{e^{x}}{x^{n}} = +\\infty$ \\\\ (n \\in \\mathbb{N}).$$
Lean4
/-- The function `exp(x)/x^n` tends to `+∞` at `+∞`, for any natural number `n` -/
theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) atTop atTop :=
by
refine (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
eventually_atTop.1
((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually (gt_mem_nhds this))
simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN
refine ⟨N, trivial, fun x hx => ?_⟩
rw [Set.mem_Ioi] at hx
have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]
calc
x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
_ ≤ exp ⌈x⌉₊ / (exp 1 * C) := (mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le)
_ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
_ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
