isBigOWith_const_mul_self

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If f is O_l(g) then c ⋅ f is O_l(g) with appropriate scaling by ∥c∥.

Русский

Если f = O_l(g), то c f = O_l(g) при нормировке константы ∥c∥.

LaTeX

$$IsBigOWith c l (fun x => c' * f x) g$$

Lean4

theorem isBigOWith_const_mul_self (c : R) (f : α → R) (l : Filter α) : IsBigOWith ‖c‖ l (fun x => c * f x) f :=
  isBigOWith_of_le' _ fun _x => norm_mul_le _ _

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

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

Разделы

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

Аффилиация

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