Proving correctness of Fast Discrete Fourier transforms

Fast Dis­crete Fouri­er Trans­forms are key al­go­rithms in sig­nal pro­cess­ing and big in­te­ger com­pu­ta­tions. Im­ple­men­ta­tion of the plain de­f­i­n­i­tion how­ev­er would re­sult in qua­drat­ic run­time. Lin­ear-log­a­rith­mic run­time is al­ways pos­si­ble, but you need a tool­box of al­go­rithms tai­lored to dif­fer­ent vec­tor sizes. The choice of the al­go­rithm de­pends on whether the vec­tor size is prime, com­pos­ite with co­prime fac­tors, or ar­bi­trary com­pos­ite. It also de­pends on con­sid­er­a­tions of data lo­cal­i­ty. There is a fall­back method, when all the oth­er ap­proach­es are too slow.

As a toy project for learn­ing Lean, I im­ple­ment­ed the com­mon Fast Fouri­er Trans­form al­go­rithms and proved their cor­rect­ness.