isLittleO_pow_sub_pow_sub — Mathlib

English

Let x0 be in a normed space. Then for m>1, ‖x−x0‖^m = o_{nhds x0}(x−x0).

Русский

Пусть x0 в нормированном пространстве. Тогда при m>1 верно ‖x−x0‖^m = o_{nhds x0}(x−x0).

LaTeX

$$$\\displaystyle \\text{If } m>1,\\; (x\\mapsto \\|x-x_0\\|^m) = o_{\\mathcal{N}_{x_0}}(x-x_0).$$$

Lean4

theorem isLittleO_pow_sub_pow_sub (x₀ : E') {n m : ℕ} (h : n < m) :
    (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => ‖x - x₀‖ ^ n :=
  (isLittleO_pow_pow h).comp_tendsto (tendsto_norm_sub_self x₀)

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