def FourierFF.dotProdAnnihilator {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (V : Submodule (ZMod p) (Fin d → ZMod p)) : Set (Fin d → ZMod p)

The annihilator (orthogonal complement) of a subspace V ⊂ 𝔽_p^d with respect to the standard dot product: V^⊥ = {ξ : ⟨ξ, v⟩ = 0 for all v ∈ V}.

noncomputable def FourierFF.cosetIndicator {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (V : Submodule (ZMod p) (Fin d → ZMod p)) (a : Fin d → ZMod p) : (Fin d → ZMod p) → ℂ

The characteristic function of the affine subspace a + V ⊂ 𝔽_p^d: it equals 1 on the coset {a + v : v ∈ V} and 0 elsewhere.

theorem FourierFF.norm_dft_cosetIndicator {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (e : AddChar (ZMod p) ℂ) (he : e ≠ 0) (V : Submodule (ZMod p) (Fin d → ZMod p)) (a ξ : Fin d → ZMod p) : ‖dft e (cosetIndicator V a) ξ‖ = if ξ ∈ dotProdAnnihilator V then ↑(Fintype.card ↥V) else 0

Lemma 2.7 (Fourier transform of the indicator of an affine plane). If P = a + V is an affine k-plane in 𝔽_p^d, then $$\bigl|\widehat{\mathbf{1}_P}(\xi)\bigr| = \begin{cases} |V| = q^k & \xi \in V^\perp \\ 0 & \xi \notin V^\perp.\end{cases}$$ The proof shifts to the linear case using the character e(-⟨ξ,a⟩), then evaluates the sum ∑_{v∈V} e(⟨ξ, v⟩) using the standard orthogonality relations for characters on the finite abelian group V.