theorem FourierFF.conj_dft {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (e : AddChar (ZMod p) ℂ) (g : (Fin d → ZMod p) → ℂ) (ξ : Fin d → ZMod p) : (starRingEnd ℂ) (dft e g ξ) = ∑ y : Fin d → ZMod p, (starRingEnd ℂ) (g y) * (fourierChar e ξ) y

The complex conjugate of the discrete Fourier transform satisfies $\overline{\hat g(\xi)} = \sum_y \overline{g(y)}\, e_\xi(y)$, swapping the additive character for its complex conjugate.

theorem FourierFF.inv_mul_fourierChar {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (e : AddChar (ZMod p) ℂ) (ξ x y : Fin d → ZMod p) : (fourierChar e ξ)⁻¹ x * (fourierChar e ξ) y = (fourierChar e ξ) (y - x)

Multiplicative property of the Fourier character: $e_\xi(x)^{-1} \cdot e_\xi(y) = e_\xi(y - x)$.

theorem FourierFF.fourierChar_swap {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (e : AddChar (ZMod p) ℂ) (a ξ : Fin d → ZMod p) : (fourierChar e ξ) a = (fourierChar e a) ξ

Symmetry of the Fourier character in its two arguments: $e_\xi(a) = e_a(\xi)$, a consequence of the symmetric dot product $a \cdot \xi = \xi \cdot a$.

theorem FourierFF.parseval {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (e : AddChar (ZMod p) ℂ) (he : e ≠ 0) (f g : (Fin d → ZMod p) → ℂ) : ∑ x : Fin d → ZMod p, f x * (starRingEnd ℂ) (g x) = (↑(Fintype.card (Fin d → ZMod p)))⁻¹ * ∑ ξ : Fin d → ZMod p, dft e f ξ * (starRingEnd ℂ) (dft e g ξ)

Parseval/Plancherel on $\mathbb{F}_q^d$ (Theorem 2.6). For $f, g : \mathbb{F}_q^d \to \mathbb{C}$ and a non-trivial additive character e, $$\sum_{x \in \mathbb{F}_q^d} f(x)\,\overline{g(x)} = \frac{1}{q^d}\, \sum_{\xi \in \mathbb{F}_q^d} \hat f(\xi)\, \overline{\hat g(\xi)}.$$