The Akra–Bazzi theorem and the Master theorem

This article contains a formalisation of the Akra–Bazzi method [1] based on a proof by Leighton [2]. It is a generalisation of the well-known Master Theorem for analysing the complexity of Divide & Con-quer algorithms. We also include a generalised version of the Master theorem based on the Akra–Bazzi theorem, which is easier to apply than the Akra–Bazzi theorem itself. Some proof methods that facilitate applying the Master theorem are also included. For a more detailed explanation of the formalisa-tion and the proof methods, see the accompanying paper (publicatio