noncomputable def ProjectionTheory.discreteProjection (p : ℕ) [NeZero p] {N : ℕ} (f : Fin N → ℂ) : ZMod p → ℂ

The projection $\pi_p f : \mathbb{Z}_p \to \mathbb{C}$ of a function $f : [N] \to \mathbb{C}$ to the discrete subgroup $\mathbb{Z}_p$: for each residue $a \in \mathbb{Z}_p$, sum the values of $f$ over all $n \in [N]$ with $n \equiv a \pmod p$.

theorem ProjectionTheory.dft_discreteProjection (p : ℕ) [NeZero p] {N : ℕ} (f : Fin N → ℂ) (α : ZMod p) : ZMod.dft (discreteProjection p f) α = ∑ n : Fin N, ZMod.stdAddChar (-(↑↑n * α)) * f n

Fourier dictionary for the discrete projection: the discrete Fourier transform of $\pi_p f$ at $\alpha \in \mathbb{Z}_p$ equals $\sum_n e(-n\alpha/p)\, f(n)$, matching $\widehat{\pi_p f}(\alpha) = \hat f(\alpha/p)$.