isLittleO_pow_pow — Mathlib

English

In a normed division ring, if m < n, the function x ↦ x^n is little-o of x^m as x → 0.

Русский

В нормированном делимом кольце, если m < n, функция x ↦ x^n есть маленькое-o по отношению к x^m при x → 0.

LaTeX

$$$\\displaystyle \\text{If } m

Lean4

theorem isLittleO_pow_pow {m n : ℕ} (h : m < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x ^ m :=
  by
  rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩
  suffices (fun x : 𝕜 => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p by simpa only [pow_add, one_pow, mul_one]
  exact IsBigO.mul_isLittleO (isBigO_refl _ _) (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

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