const_smul_left

Mathlib.Analysis.Asymptotics.Lemmas

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.const_smul_left

English

If f = O_l g and c ≠ 0, then (λ x, c • f' x) = O_l (λ x, c • g' x).

Русский

Если f = O_l g и c ≠ 0, тогда (λ x, c • f'(x)) = O_l (λ x, c • g'(x)).

LaTeX

$$$ (f =O[l] g) \land c \neq 0 \Rightarrow (\lambda x. c)·f =O[l] (\lambda x. c)·g. $$$

Lean4

theorem const_smul_left (h : f' =O[l] g) (c : R) : (c • f') =O[l] g :=
  let ⟨_b, hb⟩ := h.isBigOWith
  (hb.const_smul_left _).isBigO

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

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

Разделы

Аффилиация

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