isBigO_of_le'

Mathlib.Analysis.Asymptotics.Defs

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

English

If f = o_l g and IsBigOWith c l g k, then f = o_l k.

Русский

Если f = o_l g и IsBigOWith c l g k, тогда f = o_l k.

LaTeX

$$$f = o\; l\; g \land IsBigOWith\; c\; l\; g\; k \Rightarrow f = o\; l\; k$$$

Lean4

theorem isBigO_of_le' (hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g :=
  (isBigOWith_of_le' l hfg).isBigO

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

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

Разделы

Аффилиация

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