isBigOWith_zero

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If h1: (f1 − f2) = O_l(g) and h2: (f2 − f3) = O_l(g), then (f1 − f3) = O_l(g).

Русский

Если h1: (f1 − f2) = O_l(g) и h2: (f2 − f3) = O_l(g), то (f1 − f3) = O_l(g).

LaTeX

$$$(f_1-f_2)=O[l]\\,(f_2-f_3)=O[l]\\Rightarrow (f_1-f_3)=O[l]\\,g$$$

Lean4

theorem isBigOWith_zero (hc : 0 ≤ c) : IsBigOWith c l (fun _x => (0 : E')) g' :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simpa using mul_nonneg hc (norm_nonneg <| g' x)

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

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

Разделы

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

Аффилиация

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