Fourier transform on finite abelian groups

DefinitionDiscrete Fourier transform on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group and \(f : G \to \mathbb{C}\). The discrete Fourier transform of \(f\) is the function on the additive characters \(\psi\) of \(G\) with values in \(\mathbb{C}\) (maps with \(\psi(0) = 1\) and \(\psi(a + b) = \psi(a)\psi(b)\)) given by \(\hat f(\psi) = \sum_{x \in G} \psi(x) f(x)\).

No complex conjugate is applied to the character.

def dftFun {G : Type*} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    AddChar G ℂ → ℂ :=
  fun ψ => ∑ x : G, ψ x * f x

Used by 12

Used byDonoho–Stark uncertainty principle · Functions with small support and small Fourier support vanish · Pointwise bound from a small Fourier support · Squared-norm Plancherel identity for the finite Fourier transform · Concentration bound for the Fourier transform of a function with small support · Concentration bound for a function with small Fourier support · Translation modulates the discrete Fourier transform · Fourier inversion on a finite abelian group · Plancherel formula on a finite abelian group · The \(p = 1\) endpoint of Hausdorff–Young · Hausdorff–Young inequality on a finite abelian group · The \(p = 2\) endpoint of Hausdorff–Young (Plancherel)

TheoremFourier inversion on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group with \(|G|\) elements, let \(f : G \to \mathbb{C}\), and write \(\hat f(\psi) = \sum_{y \in G} \psi(y) f(y)\) for the discrete Fourier transform of \(f\) at an additive character \(\psi\) of \(G\) with values in \(\mathbb{C}\). Then for every \(x \in G\), \(f(x) = \frac{1}{|G|} \sum_{\psi} \overline{\psi(x)} \, \hat f(\psi)\), where \(\psi\) runs over all additive characters of \(G\) with values in \(\mathbb{C}\).

Proof: expand the transform and collapse the inner sum with the orthogonality of characters. This is the Fourier inversion formula (4.4) of K. Conrad, Characters of finite abelian groups, Section 4, https://kconrad.math.uconn.edu/blurbs/grouptheory/charthy.pdf, up to reindexing \(\psi \mapsto \psi^{-1}\) (Conrad conjugates the character in the transform rather than in the inversion sum).

public theorem dft_inversion {G : Type*} [AddCommGroup G] [Fintype G]
    (f : G → ℂ) (x : G) :
    f x = ((Fintype.card G : ℂ))⁻¹ *
      ∑ ψ : AddChar G ℂ, star (ψ x) * dftFun f ψ

Sources

• A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 2, Fourier inversion theorem.

Uses 1 · Used by 2

Statement usesDiscrete Fourier transform on a finite abelian group

Used byPointwise bound from a small Fourier support · Plancherel formula on a finite abelian group

TheoremPlancherel formula on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group with \(|G|\) elements, let \(f, g : G \to \mathbb{C}\), and write \(\hat h(\psi) = \sum_{x \in G} \psi(x) h(x)\) for the discrete Fourier transform of \(h : G \to \mathbb{C}\) at an additive character \(\psi\) of \(G\) with values in \(\mathbb{C}\). Then \(\sum_{x \in G} \overline{f(x)} \, g(x)\) equals \(\frac{1}{|G|} \sum_{\psi} \overline{\hat f(\psi)} \, \hat g(\psi)\), where \(\psi\) runs over all additive characters of \(G\) with values in \(\mathbb{C}\).

Proof: apply Fourier inversion to \(g\), exchange the finite sums, and identify the conjugated inner sum with \(\overline{\hat f(\psi)}\). K. Conrad, Characters of finite abelian groups, Section 4, proves the same identity by checking it on characters.

public theorem dft_plancherel {G : Type*} [AddCommGroup G] [Fintype G]
    (f g : G → ℂ) :
    (∑ x : G, star (f x) * g x) = ((Fintype.card G : ℂ))⁻¹ *
      ∑ ψ : AddChar G ℂ, star (dftFun f ψ) * dftFun g ψ

Sources

• A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 2, Plancherel formula.

Uses 2 · Used by 2

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesFourier inversion on a finite abelian group

Used bySquared-norm Plancherel identity for the finite Fourier transform · The \(p = 2\) endpoint of Hausdorff–Young (Plancherel)

TheoremTranslation modulates the discrete Fourier transform#✓fully proved

Let \(G\) be a finite abelian group, \(f : G \to \mathbb{C}\), \(t \in G\), and \(\psi\) an additive character of \(G\) with values in \(\mathbb{C}\), and write \(\hat h(\psi) = \sum_{x \in G} \psi(x) h(x)\) for the discrete Fourier transform of \(h : G \to \mathbb{C}\). If \(g(x) = f(x - t)\) for all \(x \in G\), then \(\hat g(\psi) = \psi(t) \hat f(\psi)\).

Proof: reindex the finite sum by \(x \mapsto x + t\) and use \(\psi(x + t) = \psi(x) \psi(t)\).

public theorem dftFun_translate {G : Type*} [AddCommGroup G] [Fintype G]
    (f : G → ℂ) (t : G) (ψ : AddChar G ℂ) :
    dftFun (fun x => f (x - t)) ψ = ψ t * dftFun f ψ

Sources

• A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 2 (translation and modulation).

Uses 1

Statement usesDiscrete Fourier transform on a finite abelian group

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.