congr_of_sub

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If (f1 − f2) = O_l(g), then f1 = O_l(g) iff f2 = O_l(g).

Русский

Если (f1 − f2) = O_l(g), то f1 = O_l(g) равно f2 = O_l(g).

LaTeX

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

Lean4

theorem congr_of_sub (h : (fun x => f₁ x - f₂ x) =O[l] g) : f₁ =O[l] g ↔ f₂ =O[l] g :=
  ⟨fun h' => (h'.sub h).congr_left fun _x => sub_sub_cancel _ _, fun h' =>
    (h.add h').congr_left fun _x => sub_add_cancel _ _⟩

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

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

Разделы

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

Аффилиация

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