Convolution on finite groups

DefinitionConvolution on a finite group#✓fully proved

For a finite group \(G\) and functions \(f, g : G \to \mathbb{C}\), the convolution \(f \ast g : G \to \mathbb{C}\) is defined by \((f \ast g)(x) = \sum_{y \in G} f(y)\, g(y^{-1} x)\) for \(x \in G\).

def conv {G : Type*} [Group G] [Fintype G] (f g : G → ℂ) : G → ℂ :=
  fun x => ∑ y : G, f y * g (y⁻¹ * x)

Used by 4

Used byConvolution theorem for one-dimensional characters · Associativity of convolution · Convolution on a finite abelian group is commutative · The delta function at the identity is a left unit for convolution

TheoremAssociativity of convolution#✓fully proved

Let \(G\) be a finite group and write \(f \ast g\) for the convolution \((f \ast g)(x) = \sum_{y \in G} f(y)\, g(y^{-1} x)\) of functions on \(G\). For all \(f, g, h : G \to \mathbb{C}\) we have \((f \ast g) \ast h = f \ast (g \ast h)\).

Proof: Expand into double sums, swap them, and reindex by left multiplication, following the finite group-algebra argument in Terras, Ch. 1.

public theorem conv_assoc {G : Type*} [Group G] [Fintype G]
    (f g h : G → ℂ) : conv (conv f g) h = conv f (conv g h)

Sources

A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 1 (the group algebra).

Uses 1

Statement usesConvolution on a finite group

TheoremThe delta function at the identity is a left unit for convolution#✓fully proved

Let \(G\) be a finite group, write \(f \ast g\) for the convolution \((f \ast g)(x) = \sum_{y \in G} f(y)\, g(y^{-1} x)\) of functions on \(G\), and let \(\delta_1 : G \to \mathbb{C}\) be given by \(\delta_1(1) = 1\) and \(\delta_1(x) = 0\) for \(x \neq 1\). Then \(\delta_1 \ast f = f\) for every \(f : G \to \mathbb{C}\).

Proof: Expand the convolution and collapse the sum at the unique nonzero value of the delta function, following the identity-element argument in Terras, Ch. 1.

public theorem conv_single_one {G : Type*} [Group G] [Fintype G]
    [DecidableEq G] (f : G → ℂ) : conv (Pi.single (1 : G) (1 : ℂ)) f = f

Sources

A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 1 (identity of the group algebra).

Uses 1

Statement usesConvolution on a finite group

TheoremConvolution on a finite abelian group is commutative#✓fully proved

Let \(G\) be a finite abelian group and write \(f \ast g\) for the convolution \((f \ast g)(x) = \sum_{y \in G} f(y)\, g(y^{-1} x)\) of functions on \(G\). For all \(f, g : G \to \mathbb{C}\) we have \(f \ast g = g \ast f\).

Proof: Reindex by \(y \mapsto y^{-1} x\) and use commutativity in \(G\) and in \(\mathbb{C}\), as in the commutative group-algebra argument in Terras, Ch. 2.

public theorem conv_comm_of_comm {G : Type*} [CommGroup G] [Fintype G]
    (f g : G → ℂ) : conv f g = conv g f

Sources

A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 2 (commutative group algebra of an abelian group).

Uses 1

Statement usesConvolution on a finite group

TheoremConvolution theorem for one-dimensional characters#✓fully proved

Let \(G\) be a finite group, let \(\varphi : G \to \mathbb{C}\) satisfy \(\varphi(1) = 1\) and \(\varphi(xy) = \varphi(x)\varphi(y)\) for all \(x, y \in G\) (a one-dimensional character), and let \(f, g : G \to \mathbb{C}\). Writing \(f \ast g\) for the convolution \((f \ast g)(x) = \sum_{y \in G} f(y)\, g(y^{-1} x)\), we have

\[ \sum_{x \in G} \varphi(x)\,(f \ast g)(x) = \Big(\sum_{x \in G} \varphi(x) f(x)\Big)\Big(\sum_{x \in G} \varphi(x) g(x)\Big). \]

Proof: Swap the finite sums, reindex by \(x = yz\), and use multiplicativity of \(\varphi\) to factor the character pairing, following Terras, Ch. 2–3.

public theorem charPair_conv {G : Type*} [Group G] [Fintype G]
    (φ : G →* ℂ) (f g : G → ℂ) :
    (∑ x : G, φ x * conv f g x) =
      (∑ x : G, φ x * f x) * (∑ x : G, φ x * g x)

Sources

A. Terras, Fourier Analysis on Finite Groups and Applications, Ch. 2–3 (the Fourier transform takes convolution to pointwise products).

Uses 1

Statement usesConvolution on a finite group

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.