isBigO_pow_pow_of_le_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

$$$$ (r_1)^n = o[atTop] (r_2)^n \\quad (n \\to \\infty) $$$$

Lean4

theorem isBigO_pow_pow_of_le_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ ≤ r₂) :
    (fun n : ℕ ↦ r₁ ^ n) =O[atTop] fun n ↦ r₂ ^ n :=
  h₂.eq_or_lt.elim (fun h ↦ h ▸ isBigO_refl _ _) fun h ↦ (isLittleO_pow_pow_of_lt_left h₁ h).isBigO

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