Discrete Fourier Transform (DFT) theorems over mathlib ℂ

TorchLean’s runtime FFT building blocks (NN.Runtime.Autograd.TorchLean.Fft) implement FFT/IFFT by explicit DFT matrices. This file proves the corresponding exact math facts over mathlib’s complex numbers ℂ:

• the inverse DFT matrix is a left inverse of the DFT matrix, and therefore
• $\operatorname{ifft}(\operatorname{fft}(x))=x$ for vectors.

We prove these statements in the mathlib Matrix world first. That choice is deliberate: primitive roots of unity, conjugate transposes, geometric sums, and matrix inverse facts already live cleanly in mathlib for ℂ.

The TorchLean runtime FFT code uses shape-indexed tensors and scalar-polymorphic twiddle factors written with cos/sin. Connecting that runtime representation to these exact matrices is a separate transport theorem in NN.Proofs.Analysis.FftBridge. Keeping the files split avoids making the pure DFT algebra import the runtime/autograd implementation.

References:

• Any standard Fourier analysis / numerical linear algebra text (this is the classical DFT inversion formula).
• For the primitive-root-of-unity facts used here, we rely on mathlib’s Complex.isPrimitiveRoot_exp and the geometric-sum identity mul_geom_sum.

DFT / IDFT matrices

noncomputable def Proofs.Fft.ζ (n : ℕ) : ℂ

Primitive n-th root of unity: $\zeta_n=\exp(2\pi i/n)$.

noncomputable def Proofs.Fft.ω (n : ℕ) : ℂ

The negative-frequency root used by the DFT: $\omega_n=\zeta_n^{-1}=\exp(-2\pi i/n)$.

noncomputable def Proofs.Fft.dftMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ

DFT matrix F : n×n (frequency × spatial), with entries:

$F_{k,j}=\omega_n^{jk}$.

This matches the usual $\exp(-2\pi ijk/n)$ convention (since $\omega_n=\exp(-2\pi i/n)$).

noncomputable def Proofs.Fft.idftMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ

Inverse DFT matrix F⁻¹ : n×n (spatial × frequency), with entries:

$F^{-1}_{j,k}=\zeta_n^{jk}/n$.

This matches the classical inverse scaling $1/n$.

Inversion theorem

The proof follows the textbook orthogonality argument. The $(i,k)$ entry of $\operatorname{IDFT}\operatorname{DFT}$ is

$$ \frac1n\sum_j\left(\zeta^i(\zeta^k)^{-1}\right)^j. $$

If $i=k$, the ratio is $1$ and the sum is $n$. If $i\ne k$, the ratio is a nontrivial $n$-th root of unity, so the geometric sum is $0$.

theorem Proofs.Fft.idft_mul_dft (n : ℕ) (hn : n ≠ 0) : idftMatrix n * dftMatrix n = 1

Main algebraic identity: $\operatorname{IDFT}\operatorname{DFT}=I$ (over ℂ), for $n\ne0$.

This is the standard DFT inversion theorem.

Orthogonality / unitary form

theorem Proofs.Fft.idftMatrix_eq_invNat_smul_conjTranspose_dftMatrix (n : ℕ) : idftMatrix n = (1 / ↑n) • (dftMatrix n).conjTranspose

On ℂ, the inverse DFT matrix is a scaled conjugate transpose of the DFT matrix:

$F^{-1}=n^{-1}F^{\mathrm H}$.

theorem Proofs.Fft.conjTranspose_dft_mul_dft (n : ℕ) (hn : n ≠ 0) : (dftMatrix n).conjTranspose * dftMatrix n = ↑n • 1

Orthogonality identity (unitary form): $F^{\mathrm H}F=nI$.

Equivalently, the DFT columns form an orthogonal basis with squared norm $n$.

theorem Proofs.Fft.dft_mul_idft (n : ℕ) (hn : n ≠ 0) : dftMatrix n * idftMatrix n = 1

Right-inverse form: $\operatorname{DFT}\operatorname{IDFT}=I$ (for $n\ne0$).

Vector form

noncomputable def Proofs.Fft.dft (n : ℕ) (x : Fin n → ℂ) : Fin n → ℂ

DFT as a linear operator on Fin n → ℂ.

noncomputable def Proofs.Fft.idft (n : ℕ) (x : Fin n → ℂ) : Fin n → ℂ

Inverse DFT as a linear operator on Fin n → ℂ.

theorem Proofs.Fft.idft_dft (n : ℕ) (hn : n ≠ 0) (x : Fin n → ℂ) : idft n (dft n x) = x

Vector inversion theorem: $\operatorname{idft}(\operatorname{dft}(x))=x$, for $n\ne0$.

theorem Proofs.Fft.dft_idft (n : ℕ) (hn : n ≠ 0) (x : Fin n → ℂ) : dft n (idft n x) = x

Vector inversion theorem (other direction): $\operatorname{dft}(\operatorname{idft}(x))=x$, for $n\ne0$.