| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Fast Fourier Transform
| Title: | Fast Fourier Transform |
| Author: | Clemens Ballarin |
| Submission date: | 2005-10-12 |
| 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. |
| BibTeX: |
@article{FFT-AFP,
author = {Clemens Ballarin},
title = {Fast Fourier Transform},
journal = {Archive of Formal Proofs},
month = oct,
year = 2005,
note = {\url{http://isa-afp.org/entries/FFT.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |