Code, paper and slides for the Coq Workshop 2015 abstract:
"Adventures in the (not so) Complex Space"
By:
- Emilio Jesús Gallego Arias
- Pierre Jouvelot
CRI, MINES ParisTech, PSL Research University
We present a constructive formalization of the Discrete Fourier Transform and some associated properties. We mainly follow https://ccrma.stanford.edu/~jos/mdft, proving shifting, convolution, unitary/energy theorems.
Some additional facts about inner products and primitive roots are included.
To install coq and ssreflect in Debian system, you can use:
$ sudo aptitude install libssreflect-coq
The paper and slides are released under a CC-BY License, the code is under CeCILL-B and (c) (c) Copyright Microsoft Corporation, Inria, and CRI MINES ParisTech, PSL Research University.