isLittleO_pow_pow_of_abs_lt_left — Mathlib

English

If |r1| < |r2|, then r1^n = o(r2^n) as n → ∞.

Русский

Если |r1| < |r2|, тогда r1^n = o(r2^n) при n → ∞.

LaTeX

$$$$ |r_1| < |r_2| \\Rightarrow (r_1)^n = o[atTop] (r_2)^n $$$$

Lean4

theorem isLittleO_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : |r₁| < |r₂|) :
    (fun n : ℕ ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n :=
  by
  refine (IsLittleO.of_norm_left ?_).of_norm_right
  exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

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