DFT Algebraic Lemmas

This file contains the algebraic identities needed for the NTT correctness proof, in particular the Danielson-Lanczos (butterfly) splitting identity and the recursive DFT definition.

noncomputable def dft {R : Type u_1} [CommRing R] (N : ℕ) (ω : R) (a : Fin N → R) (k : ℕ) : R

The DFT of a sequence a : Fin N → R with respect to a root of unity ω at index k.

Equations

• dft N ω a k = ∑ j : Fin N, a j * ω ^ (↑j * k)

theorem dft_danielson_lanczos {R : Type u_1} [CommRing R] (N : ℕ) (ω : R) (a : Fin (2 * N) → R) (k : ℕ) : dft (2 * N) ω a k = dft N (ω ^ 2) (fun (j : Fin N) => a ⟨2 * ↑j, ⋯⟩) k + ω ^ k * dft N (ω ^ 2) (fun (j : Fin N) => a ⟨2 * ↑j + 1, ⋯⟩) k

theorem dft_danielson_lanczos_second_half {R : Type u_1} [CommRing R] (N : ℕ) (ω : R) (hω : ω ^ N = -1) (a : Fin (2 * N) → R) (k : ℕ) : dft (2 * N) ω a (k + N) = dft N (ω ^ 2) (fun (j : Fin N) => a ⟨2 * ↑j, ⋯⟩) k - ω ^ k * dft N (ω ^ 2) (fun (j : Fin N) => a ⟨2 * ↑j + 1, ⋯⟩) k

noncomputable def ref_ntt {R : Type u_2} [CommRing R] (n : ℕ) (ω : R) (a : Fin (2 ^ n) → R) : Fin (2 ^ n) → R

Recursive Cooley-Tukey DFT on sequences of length 2^n. This mirrors the structure of the butterfly algorithm: recursively split into even/odd halves, compute smaller DFTs, then combine using twiddle factors.

Equations

• One or more equations did not get rendered due to their size.
• ref_ntt 0 x✝ a = a

theorem ref_ntt_eq_dft {R : Type u_1} [CommRing R] (n : ℕ) (ω : R) (hω : n = 0 ∨ ω ^ 2 ^ (n - 1) = -1) (a : Fin (2 ^ n) → R) (k : Fin (2 ^ n)) : ref_ntt n ω a k = dft (2 ^ n) ω a ↑k