Hausdorff–Young inequality on finite abelian groups

TheoremThe \(p = 1\) endpoint of Hausdorff–Young#✓fully proved

Let \(G\) be a finite abelian group and \(f : G \to \mathbb{C}\), with discrete Fourier transform \(\hat f\). For every additive character \(\psi\) of \(G\), \(|\hat f(\psi)| \le \sum_{x \in G} |f(x)|\).

theorem dftFun_sup_le {G : Type*} [AddCommGroup G] [Fintype G] (f : G → ℂ)
    (ψ : AddChar G ℂ) :
    ‖dftFun f ψ‖ ≤ ∑ x : G, ‖f x‖

Uses 1 · Used by 1

Statement usesDiscrete Fourier transform on a finite abelian group

Used byHausdorff–Young inequality on a finite abelian group

TheoremThe \(p = 2\) endpoint of Hausdorff–Young (Plancherel)#✓fully proved

Let \(G\) be a finite abelian group and let \(f : G \to \mathbb{C}\) have discrete Fourier transform \(\hat f\). Then, with \(\psi\) running over the additive characters of \(G\) and \(|G|\) the number of elements of \(G\), \(\sum_{\psi} |\hat f(\psi)|^2 = |G| \sum_{x \in G} |f(x)|^2\).

theorem sum_norm_sq_dftFun {G : Type*} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    (∑ ψ : AddChar G ℂ, ‖dftFun f ψ‖ ^ 2) =
      (Fintype.card G : ℝ) * ∑ x : G, ‖f x‖ ^ 2

Uses 2 · Used by 1

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesPlancherel formula on a finite abelian group

Used byHausdorff–Young inequality on a finite abelian group

TheoremHausdorff–Young inequality on a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group, let \(f : G \to \mathbb{C}\) have discrete Fourier transform \(\hat f\), let \(p\) be a real number with \(1 < p \le 2\), and let \(q = p/(p - 1)\). Write \(|G|\) for the number of elements of \(G\) and let \(\psi\) run over the additive characters of \(G\). Then \(\left(\sum_{\psi} |\hat f(\psi)|^q\right)^{1/q} \le |G|^{1/q} \left(\sum_{x \in G} |f(x)|^p\right)^{1/p}\).

The statement also assumes \(\sigma\)-algebras on \(G\) and on its character group in which singletons are measurable; on a finite set such a \(\sigma\)-algebra contains every subset, so this is no restriction.

theorem hausdorffYoung_dft {G : Type*} [AddCommGroup G] [Fintype G]
    [MeasurableSpace G] [MeasurableSpace (AddChar G ℂ)]
    [MeasurableSingletonClass G] [MeasurableSingletonClass (AddChar G ℂ)]
    {p : ℝ} (hp1 : 1 < p) (hp2 : p ≤ 2) (f : G → ℂ) :
    (∑ ψ : AddChar G ℂ, ‖dftFun f ψ‖ ^ (p / (p - 1))) ^ (1 / (p / (p - 1))) ≤
      (Fintype.card G : ℝ) ^ (1 / (p / (p - 1))) *
        (∑ x : G, ‖f x‖ ^ p) ^ (1 / p)

Uses 4

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesThe \(p = 1\) endpoint of Hausdorff–Young · The \(p = 2\) endpoint of Hausdorff–Young (Plancherel) · Riesz–Thorin interpolation theorem on finite sets

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.