add_isBigO

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.add_isBigO

English

If f1 = OWith c1 l g and f2 = o_l g, then f1+f2 = OWith c2 l g for some c2 > c1.

Русский

Если f1 = OWith c1 l g и f2 = o_l g, то существует c2 > c1 такое, что f1+f2 = OWith c2 l g.

LaTeX

$$$ (f_1 =OWith c_1 l g) \\land (f_2 =o[l] g) \\land (c_1 < c_2) \\Rightarrow (f_1 + f_2) =OWith c_2 l g $$$

Lean4

theorem add_isBigO (h₁ : f₁ =o[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g :=
  h₁.isBigO.add h₂

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

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

Разделы

Аффилиация

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