Master theorem for divide-and-conquer recurrences

Stream: mathlib4

[Coder-Osman]

Hi all, I’ve formalized a version of the Master Theorem for divide-and-conquer recurrences (time complexity) in Lean 4, together with supporting lemmas.
Roughly, it’s about recurrences of the form

$$T(n) = a \cdot T(\lfloor n/b \rfloor) + f(n)$$

and derives asymptotic bounds (Big-O) under standard assumptions.
I’m wondering where this should live in mathlib: would Mathlib.Analysis.Asymptotics be the right home, or is Mathlib.Combinatorics ever appropriate here? (Alternatively, if people prefer a “computational complexity” home under Mathlib/Computability, I can adapt.)
Any advice on file location / naming / existing lemmas to reuse would be appreciated!

[Yaël Dillies]

Congratulations! Does this not already exist in Mathlib.Computability.AkraBazzi ?

[Coder-Osman]

Thanks for the pointer! I honestly missed Mathlib.Computability.AkraBazzi when I was searching, so that’s my oversight.
I’ll just treat my development as a personal exercise. Really appreciate the heads-up—it saved me from reinventing the wheel.

[Snir Broshi]

Coder-Osman said:

I’ll just treat my development as a personal exercise.

Can I suggest solving this TODO in AkraBazzi?

* 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.)