English
For every natural k and every real r > 1, n^k grows strictly slower than r^n; equivalently, n^k = o(r^n) as n → ∞.
Русский
Для любого k ∈ ℕ и любого r > 1 верно, что n^k растет медленнее, чем r^n; то есть n^k = o(r^n) при n → ∞.
LaTeX
$$$\\\\forall k \\\\in \\\\mathbb{N}, \\\\forall r \\\\in \\\\mathbb{R}, 1 < r \\\\Rightarrow \\\\lim_{n \\to \\infty} \frac{n^k}{r^n} = 0$$$
Lean4
/-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`. -/
theorem isLittleO_pow_const_const_pow_of_one_lt {R : Type*} [NormedRing R] (k : ℕ) {r : ℝ} (hr : 1 < r) :
(fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ r ^ n :=
by
have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left
obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ := ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists
have h0 : 0 ≤ r' := zero_le_one.trans h1.le
suffices (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n from
this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')
conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]
suffices ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖ from (isBigO_of_le' _ this).pow _
intro n
rw [mul_right_comm]
refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))
simpa [_root_.div_eq_inv_mul, Real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1
