English
If ||r1|| < r2, then for any natural k we have n^k r1^n = o(r2^n) as n → ∞.
Русский
Если ||r1|| < r2, тогда для любого k ∈ ℕ имеем n^k r1^n = o(r2^n) при n → ∞.
LaTeX
$$$\\\\forall k \\\\in \\\\mathbb{N}, \\\\|r_1\\\\| < r_2 \\\\Rightarrow \\\\lim_{n \\to \\infty} \\\\frac{n^k r_1^n}{r_2^n} = 0$$$
Lean4
/-- If `‖r₁‖ < r₂`, then for any natural `k` we have `n ^ k r₁ ^ n = o (r₂ ^ n)` as `n → ∞`. -/
theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type*} [NormedRing R] (k : ℕ) {r₁ : R} {r₂ : ℝ}
(h : ‖r₁‖ < r₂) : (fun n ↦ (n : R) ^ k * r₁ ^ n : ℕ → R) =o[atTop] fun n ↦ r₂ ^ n :=
by
by_cases h0 : r₁ = 0
· refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl
simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]
rw [← Ne, ← norm_pos_iff] at h0
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
exact .of_norm_eventuallyLE <| eventually_norm_pow_le r₁
