noncomputable def FourierFF.dotProd {F : Type u_1} [Field F] {d : ℕ} (ξ : Fin d → F) : (Fin d → F) →+ F

The standard dot product on F^d packaged as an additive homomorphism in the first argument: x ↦ ∑ᵢ xᵢ ξᵢ.

noncomputable def FourierFF.fourierChar {F : Type u_1} [Field F] {d : ℕ} (e : AddChar F ℂ) (ξ : Fin d → F) : AddChar (Fin d → F) ℂ

The Fourier character on F^d indexed by frequency ξ: x ↦ e(⟨x, ξ⟩), built from a base additive character e on F.

@[simp]

theorem FourierFF.fourierChar_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d : ℕ} (e : AddChar F ℂ) (ξ x : Fin d → F) : (fourierChar e ξ) x = e (∑ i : Fin d, x i * ξ i)

Unfolds fourierChar e ξ x to the explicit formula e(⟨x, ξ⟩) = e(∑ᵢ xᵢ ξᵢ).

noncomputable def FourierFF.dft {F : Type u_1} [Field F] [Fintype F] {d : ℕ} (e : AddChar F ℂ) (f : (Fin d → F) → ℂ) (ξ : Fin d → F) : ℂ

Discrete Fourier transform of f : F^d → ℂ at frequency ξ: $$\hat f(\xi) = \sum_{x \in F^d} f(x) \overline{e(\langle x, \xi\rangle)}.$$

theorem FourierFF.dft_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d : ℕ} (e : AddChar F ℂ) (f : (Fin d → F) → ℂ) (ξ : Fin d → F) : dft e f ξ = ∑ x : Fin d → F, f x * e (-∑ i : Fin d, x i * ξ i)

Rewrites the DFT in terms of e(-⟨x, ξ⟩) instead of the inverse character.

theorem FourierFF.fourierChar_eq_zero_iff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d : ℕ} (e : AddChar F ℂ) (he : e ≠ 0) (a : Fin d → F) : fourierChar e a = 0 ↔ a = 0

Nondegeneracy of the Fourier character: for a nontrivial base character e, fourierChar e a is the trivial character iff a = 0.

theorem FourierFF.sum_fourierChar {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d : ℕ} (e : AddChar F ℂ) (he : e ≠ 0) (a : Fin d → F) : ∑ ξ : Fin d → F, (fourierChar e a) ξ = if a = 0 then ↑(Fintype.card (Fin d → F)) else 0

Orthogonality of characters on F^d: $$\sum_{\xi \in F^d} e(\langle a, \xi\rangle) = \begin{cases} q^d & a = 0\\ 0 & a \neq 0.\end{cases}$$

theorem FourierFF.fourier_inversion {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {d : ℕ} (e : AddChar F ℂ) (he : e ≠ 0) (f : (Fin d → F) → ℂ) (x : Fin d → F) : f x = (↑(Fintype.card (Fin d → F)))⁻¹ * ∑ ξ : Fin d → F, dft e f ξ * (fourierChar e ξ) x

Theorem 2.5 (Fourier inversion on F^d). For any f : F^d → ℂ and any x ∈ F^d, $$f(x) = \frac{1}{q^d} \sum_{\xi \in F^d} \hat f(\xi)\, e(\langle x, \xi\rangle).$$ Splitting the ξ = 0 term yields the zero-frequency / high-frequency decomposition $f = f_0 + f_h$ with $f_0 = \tfrac{1}{q^d}\hat f(0)$ constant.