isLittleO_norm_pow_norm_pow — Mathlib

English

For vectors in a normed space, if m < n then the norm of x^n is little-o of the norm of x^m as x → 0.

Русский

Для векторов в нормированном пространстве, если m < n, то нормa x^n есть маленькое-o по отношению к норме x^m при x → 0.

LaTeX

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

Lean4

theorem isLittleO_norm_pow_norm_pow {m n : ℕ} (h : m < n) : (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ m :=
  (isLittleO_pow_pow h).comp_tendsto tendsto_norm_zero

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