noncomputable def ProjectionTheory.highFreqPart {p : ℕ} [NeZero p] (g : ZMod p → ℂ) : ZMod p → ℂ

The high-frequency part of g : ZMod p → ℂ: the function g with its mean removed, $g_h(a) = g(a) - \tfrac{1}{p}\sum_b g(b)$. This is the orthogonal complement of the constant (zero-frequency) component $g_0$ in the decomposition $g = g_0 + g_h$.

theorem ProjectionTheory.dft_highFreqPart_zero {p : ℕ} [NeZero p] (g : ZMod p → ℂ) : ZMod.dft (highFreqPart g) 0 = 0

The Fourier transform of the high-frequency part vanishes at $0$: $\widehat{g_h}(0) = 0$. This is the defining property of removing the zero Fourier mode.

theorem ProjectionTheory.dft_highFreqPart_ne_zero {p : ℕ} [NeZero p] (g : ZMod p → ℂ) (α : ZMod p) (hα : α ≠ 0) : ZMod.dft (highFreqPart g) α = ZMod.dft g α

Off the zero frequency, the Fourier transform of the high-frequency part agrees with that of g: $\widehat{g_h}(\alpha) = \hat g(\alpha)$ for $\alpha \neq 0$.

theorem plancherel_zmod (p : ℕ) [NeZero p] (g : ZMod p → ℂ) : ↑p * ∑ a : ZMod p, ‖g a‖ ^ 2 = ∑ α : ZMod p, ‖ZMod.dft g α‖ ^ 2

Plancherel's identity on $\mathbb{Z}/p\mathbb{Z}$. For g : ZMod p → ℂ, $$p \sum_{a \in \mathbb{Z}/p} |g(a)|^2 = \sum_{\alpha \in \mathbb{Z}/p} |\hat g(\alpha)|^2.$$

theorem ProjectionTheory.parseval_high_freq {p : ℕ} [NeZero p] (g : ZMod p → ℂ) : ↑p * ∑ a : ZMod p, ‖highFreqPart g a‖ ^ 2 = ∑ α : ZMod p with α ≠ 0, ‖ZMod.dft g α‖ ^ 2

Parseval applied to the high-frequency part $f_h$. The $L^2$ mass of the high-frequency part is captured by the non-zero Fourier modes of g: $$p \sum_{a} |g_h(a)|^2 = \sum_{\alpha \neq 0} |\hat g(\alpha)|^2.$$