isLittleO_coe_const_pow_of_one_lt

English

The natural numbers, viewed inside the real numbers, satisfy n = o(r^n) for every r > 1.

Русский

Натуральные числа, рассматриваемые как вещественные, удовлетворяют n = o(r^n) для любого r > 1.

LaTeX

$$$\\\\forall r>1, \\\\lim_{n \\to \\infty} \\\\frac{n}{r^n} = 0$$$

Lean4

/-- For a real `r > 1` we have `n = o(r ^ n)` as `n → ∞`. -/
theorem isLittleO_coe_const_pow_of_one_lt {R : Type*} [NormedRing R] {r : ℝ} (hr : 1 < r) :
    ((↑) : ℕ → R) =o[atTop] fun n ↦ r ^ n := by
  simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr

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