isBigO_of_le

Mathlib.Analysis.Asymptotics.Defs

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

English

If for all x, ||f(x)|| ≤ c · ||g(x)||, then f = OWith c l f g.

Русский

Если для всех x выполняется ||f(x)|| ≤ c · ||g(x)||, то f = OWith c l f g.

LaTeX

$$$\forall x, \|f(x)\| \le c \cdot \|g(x)\| \Rightarrow f = OWith\; c\; l\; f\; g$$$

Lean4

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

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

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

Разделы

Аффилиация

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