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
• ifft (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 stack.

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: ζₙ = exp(2π i / n).

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

The “negative-frequency” root used by the DFT: ωₙ = ζₙ⁻¹ = exp(-2π 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] = ωₙ^(j*k).

This matches the usual exp(-2π i j*k/n) convention (since ωₙ = exp(-2π i / n)).

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

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

F⁻¹[j,k] = ζₙ^(j*k) / n.

This matches the classical inverse scaling 1/n.

Inversion theorem

The proof follows the textbook orthogonality argument. The (i,k) entry of IDFT * DFT is

(1/n) * ∑ j, (ζ^i * (ζ^k)⁻¹)^j.

If i = k, the ratio is 1 and the sum is n. If i ≠ 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: IDFT * DFT = 1 (over ℂ), for n ≠ 0.

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) • Fᴴ.

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

Orthogonality identity (unitary form): Fᴴ * F = n • 1.

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: DFT * IDFT = 1 (for n ≠ 0).

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: idft (dft x) = x, for n ≠ 0.

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

Vector inversion theorem (other direction): dft (idft x) = x, for n ≠ 0.