right_isTheta_add

Mathlib.Analysis.Asymptotics.Theta

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

English

If f1 = o_l f2, then f2 = Θ_l (f1 + f2).

Русский

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

LaTeX

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

Lean4

theorem right_isTheta_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₁ + f₂) :=
  ⟨h.right_isBigO_add, h.add_isBigO (isBigO_refl _ _)⟩

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

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

Разделы

Аффилиация

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