Proving correctness of Fast Discrete Fourier transforms

Fast Discrete Fourier Transforms are key algorithms in signal processing and big integer computations. Implementation of the plain definition however would result in quadratic runtime. Linear-logarithmic runtime is always possible, but you need a toolbox of algorithms tailored to different vector sizes. The choice of the algorithm depends on whether the vector size is prime, composite with coprime factors, or arbitrary composite. It also depends on considerations of data locality. There is a fallback method, when all the other approaches are too slow.

As a toy project for learning Lean, I implemented the common Fast Fourier Transform algorithms and proved their correctness.