def'

Mathlib.Analysis.Asymptotics.Defs

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

English

If f =o[l] g, then the norm of f is eventually bounded by the norm of g: ∀ᶠ x ∈ l, ‖f(x)‖ ≤ ‖g(x)‖.

Русский

Если f =o[l] g, то норма f ограничена наверняка относительно нормы g.

LaTeX

$$IsLittleO.eventuallyLE h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖$$

Lean4

theorem def' (h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g :=
  isBigOWith_iff.2 <| isLittleO_iff.1 h hc

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

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

Разделы

Аффилиация

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