isBigOWith_pure

Mathlib.Analysis.Asymptotics.Defs

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

English

If f = O_l g' and f = O_{l'} g', then IsBigOWith max(c,c') on l ⊔ l' holds for f relative to g'.

Русский

Если f = O_l g' и f = O_{l'} g', тогда операция supremum даёт bound с max(c,c') на l ⊔ l'.

LaTeX

$$$\text{If } f = O_l g' \text{ and } f = O_{l'} g' ,\; IsBigOWith (\max c\ c') (l ⊔ l') f g' .$$

Lean4

@[simp]
theorem isBigOWith_pure {x} : IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖ :=
  isBigOWith_iff

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

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

Разделы

Аффилиация

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