isBigO_self_const_mul — Mathlib

English

Let c be a nonzero element. Then multiplying a function by the nonzero scalar c does not change its Big-O class; i.e., f is asymptotically bounded by g up to a constant, then c f is asymptotically bounded by g by the same constant.

Русский

Пусть c ≠ 0. Тогда умножение функции на константу c не изменяет класс Big-O: если f = O_l(g), то c·f = O_l(g).

LaTeX

$$$f = O_l\left(\lambda x. c\,f(x)\right) , \; \text{если } c \neq 0.$$$

Lean4

theorem isBigO_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) : f =O[l] fun x ↦ c * f x :=
  (isBigOWith_self_const_mul hc f l).isBigO

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