isBigO_const_mul_self

Mathlib.Analysis.Asymptotics.Defs

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

English

If f = O_l(g) then ∥c∥/∥c'∥ scaling produces IsBigOWith (∥c'∥) l (c f) g.

Русский

Если f = O_l(g), константное умножение и масштабирование сохраняют порядок: IsBigOWith (∥c'∥) l (c f) g.

LaTeX

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

Lean4

theorem isBigO_const_mul_self (c : R) (f : α → R) (l : Filter α) : (fun x => c * f x) =O[l] f :=
  (isBigOWith_const_mul_self c f l).isBigO

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

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

Разделы

Аффилиация

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