TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite support-product uncertainty for the unitary DFT

Statement

Let $N \geq 1$ , let $f \in C^{Z / N Z}$ be nonzero and let $F_{N}$ be the unitary discrete Fourier transform of The unitary discrete Fourier transform on $Z / N Z$ . Writing $supp f : = {x : f (x) \neq 0}$ and $supp F_{N} f : = {k : (F_{N} f) (k) \neq 0}$ , $∣ supp f ∣ \cdot ∣ supp F_{N} f ∣ \geq N .$ At $N = 1$ the bound is equality for every nonzero $f$ . No convergence or regularity hypothesis is involved.

Facts & Assumptions

Given: An integer $N \geq 1$ and a nonzero $f \in C^{Z / N Z}$ , with $S : = supp f$ , $T : = supp F_{N} f$ , the counting inner product $⟨ g, h ⟩ = \sum_{x \in Z / N} g (x) \overline{h (x)}$ and norm $∥ g ∥_{2}^{2} = \sum_{x} ∣ g (x) ∣^{2}$ of The counting inner product on $C^{Z / N Z}$ , and the unitary transform $(F_{N} g) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} g ([x]_{N}) e^{- 2 π i k x / N}$ of The unitary discrete Fourier transform on $Z / N Z$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[F1]

Finite sums in a commutative monoid are order-independent and linear with respect to scalar multiplication, and satisfy the triangle inequality $∣ \sum_{j} z_{j} ∣ \leq \sum_{j} ∣ z_{j} ∣$ ; the standard rules for real finite sums hold (A finite sum in a commutative monoid indexed by an arbitrary finite set, Laws of finite sums and finite products). The complex triangle inequality follows by induction on the number of summands from $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F2]

Cauchy–Schwarz for the counting inner product: $∣ ⟨ g, h ⟩ ∣ \leq ∥ g ∥_{2} ∥ h ∥_{2}$ (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors, The counting inner product on $C^{Z / N Z}$ ), where $∥ g ∥_{2}^{2} = ⟨ g, g ⟩ = \sum_{x} ∣ g (x) ∣^{2}$ .

[F3]

Finite Parseval: $⟨ F_{N} g, F_{N} h ⟩ = ⟨ g, h ⟩$ for all $g, h$ ; in particular $∥ F_{N} g ∥_{2} = ∥ g ∥_{2}$ (Finite Parseval and Plancherel identity for the unitary DFT).

[F4]

The modulus satisfies $∣ z ∣^{2} = z \overline{z} \geq 0$ and vanishes only at $z = 0$ ; complexes form a field (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

Proof

technique · direct

1.1F3F4given

The two supports. Since $f \neq 0$ there is a class with $f (x) \neq 0$ , so $S \neq \emptyset$ and $∥ f ∥_{2}^{2} = \sum_{x} ∣ f (x) ∣^{2} > 0$ by [F4]. Applying [F3] with $g = h = f$ and restricting the sum over all classes to the support $T$ , $\sum_{k \in T} ∣ (F_{N} f) (k) ∣^{2} = ∥ F_{N} f ∥_{2}^{2} = ∥ f ∥_{2}^{2} > 0,$ so $T \neq \emptyset$ as well.

1.2F1F2given

Pointwise bound on the support of the transform. For $k \in T$ , the triangle inequality and the normalisation $N^{- 1 / 2}$ of the transform give $∣ (F_{N} f) (k) ∣ \leq N^{- 1 / 2} \sum_{x \in S} ∣ f (x) ∣,$ the sum running only over $S$ because the remaining summands vanish. Cauchy–Schwarz [F2] applied on $Z / N Z$ to $u (x) = ∣ f (x) ∣$ and $v (x) = 1_{S} (x)$ gives $\sum_{x \in S} ∣ f (x) ∣ = ⟨ u, v ⟩ \leq ∥ u ∥_{2} ∥ v ∥_{2} = ∣ S ∣^{1 / 2} ∥ f ∥_{2}$ . Hence $∣ (F_{N} f) (k) ∣ \leq N^{- 1 / 2} ∣ S ∣^{1 / 2} ∥ f ∥_{2}$ for every $k \in T$ .

2.1F1F3step 1.1step 1.2

Summing over the support. Squaring the bound of step 1.2 and summing over the $∣ T ∣$ classes of $T$ gives $∥ F_{N} f ∥_{2}^{2} = \sum_{k \in T} ∣ (F_{N} f) (k) ∣^{2} \leq ∣ T ∣ N^{- 1} ∣ S ∣ ∥ f ∥_{2}^{2} .$ By Parseval [F3] the left side is $∥ f ∥_{2}^{2}$ , and step 1.1 gives $∥ f ∥_{2}^{2} > 0$ , so dividing yields $∣ S ∣ ∣ T ∣ \geq N$ .

3.1step 2.1given∎

The case $N = 1$ and conclusion. If $N = 1$ the group $Z / 1 Z$ has the single class $[0]$ , $N^{- 1 / 2} = 1$ and $e^{- 2 π i \cdot 0 \cdot 0} = 1$ , so $(F_{N} f) ([0]) = f ([0])$ ; hence $T = S = {[0]}$ for nonzero $f$ and $∣ S ∣ ∣ T ∣ = 1 = N$ , an equality. Together with step 2.1 this proves the claim for every $N \geq 1$ .

Depends on

Used by

Both finite supports cannot be singletons when N>1 Counterexample
Delta and constant functions are finite DFT extremisers Example
Uncertainty principles measure different notions of localisation Remark

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Michael E. Taylor, Fourier Analysis, Distributions, and Constant-Coefficient Linear PDE (author PDF) (standard reference, not scraped)
Terence Tao, An Uncertainty Principle for Cyclic Groups of Prime Order, Math. Res. Lett. 12 (2005) 121–127 (arXiv:math/0308286) (standard reference, not scraped)