Master theorem

This project’s goal is to formalize a proof of the Master theorem for divide-and-conquer recurrences. Along with the Master theorem, we also state definitions and some properties of the Big-O and its sibling notations.

We use original and standard definitions of the Big-O notation [ 1 , 4 , 5 ] , as well as Knuth’s definition of Big-Omega and Big-Theta [ 3 ] . We use a slightly adapted formulation of the Master Theorem from Cormen et al. [ 2 ] , with the difference being due to our use of functions on natural numbers as opposed to their more general formulation. The idea of the formalized proof is also adapted from the same source, but their proof skips many technical steps, so our proof appears to hold little resemblance.