Commit 2023-11-24 23:28 a785b32d

feat: Asymptotic order of divide-and-conquer recurrences (Akra-Bazzi theorem) (#6583) This PR proves the Akra-Bazzi theorem, which gives the asymptotic order of divide-and-conquer recurrences of the form

T n = (∑ i in Fin k, a i * T (r i n)) + g n

where T : ℕ → ℝ, and where r i n is close to b i * n for a set of coefficients b : Fin k → ℝ. These recurrences arise mainly in the analysis of divide-and-conquer algorithms such as mergesort or Strassen's algorithm for matrix multiplication. Note that the traditional proof first proves a continuous version (i.e. for T : ℝ → ℝ) and then discretizes it to get a version that is relevant for algorithms. Here we prove the discrete version directly, which shortens the proof considerably.