isTheta_asympBound

Mathlib.Computability.AkraBazzi.AkraBazzi

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.isTheta_asympBound

← MathLib Explorer

English

The isTheta_asympBound theorem states that T = Θ(asympBound g a b); equivalence of growth rates in the AB setting.

Русский

Теорема isTheta_asympBound: T = Θ(asympBound g a b).

LaTeX

$$T =Θ(atTop) asympBound(g,a,b)$$

Lean4

/-- The **Akra-Bazzi theorem**: `T ∈ Θ(n^p (1 + ∑_u^n g(u) / u^{p+1}))` -/
theorem isTheta_asympBound : T =Θ[atTop] asympBound g a b :=
  ⟨R.isBigO_asympBound, R.isBigO_symm_asympBound⟩

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

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

Разделы

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

Аффилиация

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