Divide-and-conquer recurrences and the Akra-Bazzi theorem #

A divide-and-conquer recurrence is a function T : ℕ → ℝ that satisfies a recurrence relation of the form T(n) = ∑_{i=0}^{k-1} a_i T(r_i(n)) + g(n) for large enough n, where r_i(n) is some function where ‖r_i(n) - b_i n‖ ∈ o(n / (log n)^2) for every i, the a_i's are some positive coefficients, and the b_i's are reals ∈ (0,1). (Note that this can be improved to O(n / (log n)^(1+ε)), this is left as future work.) These recurrences arise mainly in the analysis of divide-and-conquer algorithms such as mergesort or Strassen's algorithm for matrix multiplication. This class of algorithms works by dividing an instance of the problem of size n, into k smaller instances, where the i'th instance is of size roughly b_i n, and calling itself recursively on those smaller instances. T(n) then represents the running time of the algorithm, and g(n) represents the running time required to actually divide up the instance and process the answers that come out of the recursive calls. Since virtually all such algorithms produce instances that are only approximately of size b_i n (they have to round up or down at the very least), we allow the instance sizes to be given by some function r_i(n) that approximates b_i n.

The Akra-Bazzi theorem gives the asymptotic order of such a recurrence: it states that T(n) ∈ Θ(n^p (1 + ∑_{u=0}^{n-1} g(n) / u^{p+1})), where p is the unique real number such that ∑ a_i b_i^p = 1.

Main definitions and results #

asympBound: The asymptotic bound satisfied by an Akra-Bazzi recurrence, namely n^p (1 + ∑ g(u) / u^(p+1))
isTheta_asympBound: The main result stating that T(n) ∈ Θ(n^p (1 + ∑_{u=0}^{n-1} g(n) / u^{p+1}))

Implementation #

Note that the original version of the theorem has an integral rather than a sum in the above expression, and first considers the T : ℝ → ℝ case before moving on to ℕ → ℝ. We prove the above version with a sum, as it is simpler and more relevant for algorithms.

TODO #

Specialize this theorem to the very common case where the recurrence is of the form T(n) = ℓT(r_i(n)) + g(n) where g(n) ∈ Θ(n^t) for some t. (This is often called the "master theorem" in the literature.)
Add the original version of the theorem with an integral instead of a sum.

References #

Mohamad Akra and Louay Bazzi, On the solution of linear recurrence equations
Tom Leighton, Notes on better master theorems for divide-and-conquer recurrences
Manuel Eberl, Asymptotic reasoning in a proof assistant

Definition of Akra-Bazzi recurrences #

This section defines the predicate AkraBazziRecurrence T g a b r which states that T satisfies the recurrence T(n) = ∑_{i=0}^{k-1} a_i T(r_i(n)) + g(n) with appropriate conditions on the various parameters.

Technical lemmas #

The next several lemmas are technical lemmas leading up to rpow_p_mul_one_sub_smoothingFn_le and rpow_p_mul_one_add_smoothingFn_ge, which are key steps in the main proof.