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 sufficiently large n, where r_i(n) is a function such that ‖r_i(n) - b_i n‖ ∈ o(n / (log n)^2) for every i, the coefficients a_i are positive, and the coefficients b_i are real numbers in (0, 1). (This assumption can be relaxed to O(n / (log n)^(1+ε)), for some ε > 0; we leave this 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 divide the instance and process the answers produced by the recursive calls. Since virtually all such algorithms produce instances that are only approximately of size b_i n (they must round up or down, at the very least), we allow the instance sizes to be given by a 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

• 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 Akra–Bazzi theorem uses an integral rather than the sum in the above expression, and first considers the T : ℝ → ℝ case before moving on to ℕ → ℝ. We prove the version with a sum here, as it is simpler and more relevant for algorithms.

TODO

• Relax the assumption described in the introduction from o(n / (log n)^2) to O(n / (log n)^(1+ε)), for some ε > 0.
• 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

Technical lemmas

The next several lemmas are technical results 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.

theorem AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : (deriv fun (z : ℝ) => z ^ p * (1 - smoothingFn z)) =ᶠ[Filter.atTop] fun (z : ℝ) => p * z ^ (p - 1) * (1 - smoothingFn z) + z ^ (p - 1) / Real.log z ^ 2

theorem AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : (deriv fun (z : ℝ) => z ^ p * (1 + smoothingFn z)) =ᶠ[Filter.atTop] fun (z : ℝ) => p * z ^ (p - 1) * (1 + smoothingFn z) - z ^ (p - 1) / Real.log z ^ 2

theorem AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (deriv fun (z : ℝ) => z ^ p * (1 - smoothingFn z)) fun (z : ℝ) => p * z ^ (p - 1)

theorem AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (deriv fun (z : ℝ) => z ^ p * (1 + smoothingFn z)) fun (z : ℝ) => p * z ^ (p - 1)

theorem AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) : (fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 - smoothingFn z)) x‖) =Θ[Filter.atTop] fun (z : ℝ) => z ^ (p - 1)

theorem AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) : (fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 + smoothingFn z)) x‖) =Θ[Filter.atTop] fun (z : ℝ) => z ^ (p - 1)

theorem AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : GrowsPolynomially fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 - smoothingFn z)) x‖

theorem AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : GrowsPolynomially fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 + smoothingFn z)) x‖

theorem AkraBazziRecurrence.isBigO_apply_r_sub_b {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (q : ℝ → ℝ) (hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)) (hq_poly : GrowsPolynomially fun (x : ℝ) => ‖deriv q x‖) (i : α) : (fun (n : ℕ) => q ↑(r i n) - q (b i * ↑n)) =O[Filter.atTop] fun (n : ℕ) => deriv q ↑n * (↑(r i n) - b i * ↑n)

theorem AkraBazziRecurrence.rpow_p_mul_one_sub_smoothingFn_le {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ^ p a b * (1 - smoothingFn ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - smoothingFn ↑n)

theorem AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_ge {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + smoothingFn ↑n) ≤ ↑(r i n) ^ p a b * (1 + smoothingFn ↑(r i n))

Main proof

This final section proves the Akra-Bazzi theorem.

theorem AkraBazziRecurrence.base_nonempty {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) {n : ℕ} (hn : 0 < n) : (Finset.Ico ⌊b (min_bi b) / 2 * ↑n⌋₊ n).Nonempty

theorem AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =O[Filter.atTop] fun (n : ℕ) => (1 - smoothingFn ↑n) * asympBound g a b n

The main proof of the upper-bound part of the Akra-Bazzi theorem. The factor 1 - ε n does not change the asymptotic order, but it is needed for the induction step to go through.

theorem AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : (fun (n : ℕ) => (1 + smoothingFn ↑n) * asympBound g a b n) =O[Filter.atTop] T

The main proof of the lower-bound part of the Akra-Bazzi theorem. The factor 1 + ε n does not change the asymptotic order, but it is needed for the induction step to go through.

theorem AkraBazziRecurrence.isBigO_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =O[Filter.atTop] asympBound g a b

The Akra-Bazzi theorem: T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))

theorem AkraBazziRecurrence.isBigO_symm_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : asympBound g a b =O[Filter.atTop] T

The Akra-Bazzi theorem: T ∈ Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))

theorem AkraBazziRecurrence.isTheta_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =Θ[Filter.atTop] asympBound g a b

The Akra-Bazzi theorem: T ∈ Θ(n^p (1 + ∑_u^n g(u) / u^{p+1}))