add_isTheta

Mathlib.Analysis.Asymptotics.Theta

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

English

If f1 = Θ_l g and f2 = o_l g, then f1 + f2 = Θ_l g (same as previous with swapped roles).

Русский

Если 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_isTheta {f₁ f₂ : α → E'} {g : α → F} (ho : f₁ =o[l] g) (hΘ : f₂ =Θ[l] g) : (f₁ + f₂) =Θ[l] g :=
  add_comm f₁ f₂ ▸ hΘ.add_isLittleO ho

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

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

Разделы

Аффилиация

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