English
The isBigO_symm_asympBound shows symmetry: asympBound = O(T) and T = O(asympBound), hence T ∈ Θ(asympBound).
Русский
Симметрия: асимп Bound эквивалентен T с обеих сторон, значит T ∈ Θ(asympBound).
LaTeX
$$asympBound(g,a,b) = O(T) and T = O(asympBound(g,a,b))$$
Lean4
/-- The **Akra-Bazzi theorem**: `T ∈ Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))` -/
theorem isBigO_symm_asympBound : asympBound g a b =O[atTop] T := by
calc
asympBound g a b
_ = (fun n => 1 * asympBound g a b n) := by simp
_ ~[atTop] (fun n => (1 + ε n) * asympBound g a b n) :=
by
refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl
rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero, ←
Function.comp_def (fun n => 1 + ε n) Nat.cast]
exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const tendsto_natCast_atTop_atTop
_ =O[atTop] T := R.smoothingFn_mul_asympBound_isBigO_T
