isLittleO_zero

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isLittleO_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]\,g\\;\\land\\; (f_2-f_3)=o[l]\,g\\Rightarrow (f_1-f_3)=o[l]\,g$$$

Lean4

theorem isLittleO_zero : (fun _x => (0 : E')) =o[l] g' :=
  IsLittleO.of_bound fun c hc => univ_mem' fun x => by simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

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

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

Разделы

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

Аффилиация

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