English
The Akra–Bazii theorem asserts that T is Θ(asympBound g a b); i.e., T has the same asymptotic growth as the bounding function asympBound.
Русский
Теорема Акры-Баззи утверждает, что T имеет порядок роста Θ(asympBound g a b).
LaTeX
$$T = Θ(atTop) asympBound(g,a,b).$$
Lean4
/-- The **Akra-Bazzi theorem**: `T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))` -/
theorem isBigO_asympBound : T =O[atTop] asympBound g a b := by
calc
T
_ =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by exact R.T_isBigO_smoothingFn_mul_asympBound
_ =O[atTop] (fun n => 1 * asympBound g a b n) :=
by
refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero) (isBigO_refl _ _)
rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]
exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const tendsto_natCast_atTop_atTop
_ = asympBound g a b := by simp
