Donoho–Stark uncertainty principle

TheoremSquared-norm Plancherel identity for the finite Fourier transform#✓fully proved

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

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

Uses 2 · Used by 2

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesPlancherel formula on a finite abelian group

Used byPointwise bound from a small Fourier support · Concentration bound for the Fourier transform of a function with small support

TheoremPointwise bound from a small Fourier support#✓fully proved

Let \(G\) be a finite abelian group, let \(f : G \to \mathbb{C}\), and let \(B\) be a set of additive characters of \(G\) such that the discrete Fourier transform \(\hat f\) vanishes outside \(B\). Then for every \(x \in G\), \(|f(x)|^2 \le \frac{|B|}{|G|} \sum_{y \in G} |f(y)|^2\).

theorem norm_sq_le_of_dftFun_eq_zero_of_notMem {f : G → ℂ}
    {B : Finset (AddChar G ℂ)} (hB : ∀ ψ, ψ ∉ B → dftFun f ψ = 0) (x : G) :
    ‖f x‖ ^ 2 ≤ (B.card / Fintype.card G) * ∑ y : G, ‖f y‖ ^ 2

Uses 3 · Used by 1

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesFourier inversion on a finite abelian group · Squared-norm Plancherel identity for the finite Fourier transform

Used byConcentration bound for a function with small Fourier support

TheoremConcentration bound for a function with small Fourier support#✓fully proved

Let \(G\) be a finite abelian group, let \(f : G \to \mathbb{C}\), and let \(B\) be a set of additive characters of \(G\) such that the discrete Fourier transform \(\hat f\) vanishes outside \(B\). Then for every \(A \subseteq G\), \(\sum_{x \in A} |f(x)|^2 \le \frac{|A| \cdot |B|}{|G|} \sum_{x \in G} |f(x)|^2\).

theorem sum_norm_sq_le_of_dftFun_eq_zero_of_notMem {f : G → ℂ}
    {A : Finset G} {B : Finset (AddChar G ℂ)}
    (hB : ∀ ψ, ψ ∉ B → dftFun f ψ = 0) :
    ∑ x ∈ A, ‖f x‖ ^ 2 ≤ (A.card * B.card / Fintype.card G) * ∑ x : G, ‖f x‖ ^ 2

Uses 2 · Used by 1

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesPointwise bound from a small Fourier support

Used byDonoho–Stark uncertainty principle

TheoremConcentration bound for the Fourier transform of a function with small support#✓fully proved

Let \(G\) be a finite abelian group, let \(A \subseteq G\), let \(B\) be any set of additive characters of \(G\), and let \(f : G \to \mathbb{C}\) vanish outside \(A\), with discrete Fourier transform \(\hat f\). Then \(\sum_{\psi \in B} |\hat f(\psi)|^2 \le \frac{|A| \cdot |B|}{|G|} \sum_{\psi} |\hat f(\psi)|^2\), where the last sum runs over all additive characters \(\psi\) of \(G\).

theorem sum_norm_sq_dftFun_le_of_eq_zero_of_notMem {f : G → ℂ}
    {A : Finset G} {B : Finset (AddChar G ℂ)}
    (hA : ∀ x, x ∉ A → f x = 0) :
    ∑ ψ ∈ B, ‖dftFun f ψ‖ ^ 2
      ≤ (A.card * B.card / Fintype.card G) * ∑ ψ : AddChar G ℂ, ‖dftFun f ψ‖ ^ 2

Uses 2

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesSquared-norm Plancherel identity for the finite Fourier transform

TheoremDonoho–Stark uncertainty principle#✓fully proved

Let \(G\) be a finite abelian group and let \(f : G \to \mathbb{C}\) be a nonzero function with discrete Fourier transform \(\hat f\). Then \(|G| \le |\{x \in G : f(x) \neq 0\}| \cdot |\{\psi : \hat f(\psi) \neq 0\}|\), where \(\psi\) ranges over the additive characters of \(G\).

theorem card_le_mul_card_filter_support {f : G → ℂ} (hf : f ≠ 0) :
    Fintype.card G ≤
      (Finset.univ.filter (fun x => f x ≠ 0)).card *
        (Finset.univ.filter (fun ψ => dftFun f ψ ≠ 0)).card

Uses 2 · Used by 1

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesConcentration bound for a function with small Fourier support

Used byFunctions with small support and small Fourier support vanish

TheoremFunctions with small support and small Fourier support vanish#✓fully proved

Let \(G\) be a finite abelian group, let \(A \subseteq G\), and let \(B\) be a set of additive characters of \(G\) with \(|A| \cdot |B| < |G|\). If \(f : G \to \mathbb{C}\) vanishes outside \(A\) and its discrete Fourier transform \(\hat f\) vanishes outside \(B\), then \(f = 0\).

theorem eq_zero_of_card_mul_card_lt_card {f : G → ℂ}
    {A : Finset G} {B : Finset (AddChar G ℂ)}
    (hA : ∀ x, x ∉ A → f x = 0) (hB : ∀ ψ, ψ ∉ B → dftFun f ψ = 0)
    (h : A.card * B.card < Fintype.card G) : f = 0

Uses 2

Statement usesDiscrete Fourier transform on a finite abelian group

Proof usesDonoho–Stark uncertainty principle

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.