Young's convolution inequality on finite groups

DefinitionConvolution on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group. The convolution of functions \(f, g : G \to \mathbb{C}\) is the function \(f * g : G \to \mathbb{C}\) given by \((f * g)(x) = \sum_{y \in G} f(y)\,g(x - y)\), with no normalizing factor \(1/|G|\), where \(|G|\) is the number of elements of \(G\).

noncomputable def finGroupConv {G : Type*} [AddCommGroup G] [Fintype G] (f g : G → ℂ) :
    G → ℂ :=
  fun x => ∑ y, f y * g (x - y)

Used by 4

Used byConvolution on a finite abelian group is associative · Convolution on a finite abelian group is commutative · The delta function is a left identity for convolution · Young's convolution inequality on a finite abelian group

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

For a finite abelian group \(G\) and functions \(f, g : G \to \mathbb{C}\), we have \(f * g = g * f\), where the convolution is \((f * g)(x) = \sum_{y \in G} f(y)\,g(x - y)\).

theorem finGroupConv_comm {G : Type*} [AddCommGroup G] [Fintype G] (f g : G → ℂ) :
    finGroupConv f g = finGroupConv g f

Uses 1

Statement usesConvolution on a finite abelian group

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

For a finite abelian group \(G\) and functions \(f, g, h : G \to \mathbb{C}\), we have \((f * g) * h = f * (g * h)\), where the convolution is \((f * g)(x) = \sum_{y \in G} f(y)\,g(x - y)\).

theorem finGroupConv_assoc {G : Type*} [AddCommGroup G] [Fintype G] (f g h : G → ℂ) :
    finGroupConv (finGroupConv f g) h = finGroupConv f (finGroupConv g h)

Uses 1

Statement usesConvolution on a finite abelian group

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

Let \(G\) be a finite abelian group and let \(\delta_0 : G \to \mathbb{C}\) be the function with \(\delta_0(0) = 1\) and \(\delta_0(y) = 0\) for \(y \ne 0\). Then \(\delta_0 * g = g\) for every \(g : G \to \mathbb{C}\), where the convolution is \((f * g)(x) = \sum_{y \in G} f(y)\,g(x - y)\).

theorem finGroupConv_delta_left {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    (g : G → ℂ) :
    finGroupConv (fun y => if y = 0 then (1 : ℂ) else 0) g = g

Uses 1

Statement usesConvolution on a finite abelian group

TheoremYoung's convolution inequality on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group and, for \(u : G \to \mathbb{C}\) and real \(s > 0\), write \(\|u\|_s = \left(\sum_{x \in G} |u(x)|^s\right)^{1/s}\). Let \(f, g : G \to \mathbb{C}\) and let \(p, q, r\) be real numbers with \(p > 1\), \(q > 1\), \(r > 1\) and \(1/p + 1/q = 1 + 1/r\). Then the convolution \((f * g)(x) = \sum_{y \in G} f(y)\,g(x - y)\) satisfies \(\|f * g\|_r \le \|f\|_p \, \|g\|_q\).

theorem young_convolution_finite_group {G : Type*} [AddCommGroup G] [Fintype G]
    {f g : G → ℂ} {p q r : ℝ}
    (hp : 1 < p) (hq : 1 < q) (hr : 1 < r)
    (hexp : p⁻¹ + q⁻¹ = 1 + r⁻¹) :
    (∑ x, ‖finGroupConv f g x‖ ^ r) ^ (1 / r)
      ≤ (∑ x, ‖f x‖ ^ p) ^ (1 / p) * (∑ x, ‖g x‖ ^ q) ^ (1 / q)

Uses 1

Statement usesConvolution on a finite abelian group

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.