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 Parseval and Plancherel identity for the unitary DFT

Statement

Let $N \geq 1$ and $f, g \in C^{Z / N}$ . Then

$⟨ F_{N} f, F_{N} g ⟩ = ⟨ f, g ⟩,$

where both pairings are the counting inner products of The counting inner product on $C^{Z / N Z}$ . In particular

$\sum_{k = 0}^{N - 1} ∣ (F_{N} f) (k) ∣^{2} = \sum_{x = 0}^{N - 1} ∣ f (x) ∣^{2},$

so $F_{N}$ preserves the counting inner product; invertibility of $F_{N}$ is not asserted here.

Facts & Assumptions

Given: A natural number $N \geq 1$ , functions $f, g \in C^{Z / N}$ , and classes $x, y \in Z / N Z$ .

[F1]

$F_{N} h (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} h ([x]_{N}) e^{- 2 π i k x / N}$ (The unitary discrete Fourier transform on $Z / N Z$ ); $⟨ u, v ⟩ = \sum_{z \in Z / N} u (z) \overline{v (z)}$ is the counting inner product (The counting inner product on $C^{Z / N Z}$ ).

[F2]

$\sum_{k = 0}^{N - 1} e^{2 π i (a - b) k / N} = N$ when $a \equiv b (m o d N)$ and $0$ otherwise (Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$ ).

[F3]

Finite sums over $Z / N Z$ are computed from any enumeration, are invariant under reindexing along a bijection, split over disjoint unions, satisfy the finite Fubini rule, and carry scalar factors (A finite sum in a commutative monoid indexed by an arbitrary finite set, Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule); the classes $[0]_{N}, \dots, [N - 1]_{N}$ enumerate the group (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ ).

[L1]

$\exp (u + v) = \exp u \exp v$ and $\exp w = 1$ exactly for $w \in 2 π i Z$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

[L2]

Conjugation and modulus: $\overline{z + w} = \overline{z} + \overline{w}$ , $\overline{z w} = \overline{z} \overline{w}$ , $z \overline{z} = ∣ z ∣^{2}$ , $∣ z ∣ = 0 ⟺ z = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive); $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L3]

Rational powers: $N^{- 1 / 2} N^{- 1 / 2} = N^{- 1}$ and $N^{- 1} N = 1$ (Rational powers $a^{r}$ of a positive base, Laws of rational exponents); the field laws of $C$ ( $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.1F1F2F3L1L2L3

Conjugation of the second factor: for each class $k$ , $\overline{(F_{N} g) (k)} = N^{- 1 / 2} \sum_{y = 0}^{N - 1} \overline{g ([y]_{N})} e^{2 π i k y / N}$ . Indeed, conjugation is additive and multiplicative and fixes the real scalar $N^{- 1 / 2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Laws of rational exponents); and $\overline{e^{- 2 π i k y / N}} = e^{2 π i k y / N}$ , because for $ζ = e^{i θ}$ with $θ = - 2 π k y / N$ one has $∣ ζ ∣ = 1$ by [L2] and hence $\overline{ζ} = ∣ ζ ∣^{2} / ζ = ζ^{- 1} = e^{- i θ}$ .

1.2F2

The orthogonality sum: $\sum_{k = 0}^{N - 1} e^{- 2 π i k (x - y) / N} = N$ when $[x] = [y]$ and $0$ otherwise, by [F2] with the integers $y$ and $x$ in the roles of the two congruence parameters.

1.3F3

Collapsing a sum supported at one class: for any $c : Z / N Z \to C$ and class $a$ , $\sum_{y \in Z / N} c (y) \cdot (N if y = a, 0 otherwise) = N c (a)$ ; split the index set into ${a}$ and its complement by [F3], the complement contributing $0$ because every term there has the factor $0_{C}$ .

2.1F1F3L1L3step 1.1

Expanding the pairing: substituting [F1] for both transforms, step 1.1 for the conjugate factor, and interchanging the finite sums by [F3] gives $⟨ F_{N} f, F_{N} g ⟩ = N^{- 1} \sum_{x = 0}^{N - 1} \sum_{y = 0}^{N - 1} f ([x]_{N}) \overline{g ([y]_{N})} \sum_{k = 0}^{N - 1} e^{- 2 π i k (x - y) / N}$ , where the exponentials combine by the addition law [L1] and the scalar is $N^{- 1 / 2} N^{- 1 / 2} = N^{- 1}$ by [L3].

3.1F1F3L2L3step 1.2step 1.3step 2.1∎

Evaluating the inner sum by step 1.2 and then collapsing the outer sum by step 1.3 gives $⟨ F_{N} f, F_{N} g ⟩ = N^{- 1} \sum_{x = 0}^{N - 1} N f ([x]_{N}) \overline{g ([x]_{N})} = \sum_{x = 0}^{N - 1} f ([x]_{N}) \overline{g ([x]_{N})} = ⟨ f, g ⟩$ by [L3] and the standard-representative form of the counting inner product [F1]. Taking $g = f$ and using $z \overline{z} = ∣ z ∣^{2}$ from [L2], the same computation gives $\sum_{k} ∣ (F_{N} f) (k) ∣^{2} = \sum_{x} ∣ f ([x]_{N}) ∣^{2}$ ; both assertions are proved.

Remarks

Isometry versus unitary isomorphism. The identity proved here says that $F_{N}$ preserves the counting inner product; it does not by itself assert that $F_{N}$ is bijective, and none of its steps uses inversion. Invertibility is the separate content of the inversion theorem on this page, and [L2] alone does not supply it.
Both sides use the same weight. There is no factor $1 / N$ on either side of the displayed identity, and the cancellation of the two $N^{- 1 / 2}$ factors against the orthogonality value $N$ is the only place where the normalisation is used. In Taylor's convention the same computation reads as the unitarity of $Φ_{n}$ between the $(1 / n)$ -weighted space on $Γ_{n}$ and the counting-measure space on $Z_{n}$ (11.5).

Depends on

Used by

The unitary DFT for N=1 and N=2 Example
Finite support-product uncertainty for the unitary DFT Theorem

Dependency tree · two levels

77 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)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)