add_isLittleO

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.add_isLittleO

← MathLib Explorer

English

If f1 = Θ_l g and f2 = o_l g, then f1 + f2 = Θ_l g.

Русский

Если f1 = Θ_l g и f2 = o_l g, то f1 + f2 = Θ_l g.

LaTeX

$$$\forall f_1,f_2,g:\; f_1 =\Theta_{\ell} g \land f_2 =o_{\ell} g \implies (f_1+f_2) =\Theta_{\ell} g$$$

Lean4

theorem add_isLittleO {f₁ f₂ : α → E'} {g : α → F} (hΘ : f₁ =Θ[l] g) (ho : f₂ =o[l] g) : (f₁ + f₂) =Θ[l] g :=
  (ho.trans_isTheta hΘ.symm).right_isTheta_add'.symm.trans hΘ

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

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

Разделы

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

Аффилиация

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