of_pow

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.of_pow

← MathLib Explorer

English

If f^n = o_l g^n for some n ≠ 0, then f = o_l g.

Русский

Если f^n = o_l g^n для некоторого n ≠ 0, тогда f = o_l g.

LaTeX

$$$(f^n) =o_l(g^n) \\land n \\neq 0 \\Rightarrow f =o_l g.$$$

Lean4

theorem of_pow [NormOneClass S] {f : α → S} {g : α → R} {n : ℕ} (h : (f ^ n) =o[l] (g ^ n)) (hn : n ≠ 0) : f =o[l] g :=
  IsLittleO.of_isBigOWith fun _c hc => (h.def' <| pow_pos hc _).of_pow hn le_rfl hc.le

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru