isLittleO_pow_pow_of_lt_left — Mathlib

English

If 0 ≤ r1 ≤ r2, then r1^n = O(r2^n) as n → ∞.

Русский

Если 0 ≤ r1 ≤ r2, то r1^n = O(r2^n) при n → ∞.

LaTeX

$$$$\\\\forall r_1,r_2 \\in \\mathbb{R}, \\; 0 \\le r_1 \\le r_2 \\; \\\\Rightarrow \\\\ (r_1)^n = O((r_2)^n) \\\\text{ as } n \\to \\infty.$$$$

Lean4

theorem isLittleO_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :
    (fun n : ℕ ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n :=
  have H : 0 < r₂ := h₁.trans_lt h₂
  (isLittleO_of_tendsto fun _ hn ↦ False.elim <| H.ne' <| pow_eq_zero hn) <|
    (tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr fun _ ↦
      div_pow _ _ _

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