| Abstract: |
We formalise a functional implementation of the FFT algorithm
over the complex numbers, and its inverse. Both are shown
equivalent to the usual definitions
of these operations through Vandermonde matrices. They are also
shown to be inverse to each other, more precisely, that composition
of the inverse and the transformation yield the identity up to a
scalar.
|