LemmaStatement: 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.

The DFT turns cyclic convolution into a scaled pointwise product

Statement

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

$(F_{N} (f * g)) (k) = \sqrt{N} (F_{N} f) (k) (F_{N} g) (k),$

where $*$ is the unnormalised cyclic convolution of The unnormalised cyclic convolution on $Z / N Z$ and $\sqrt{N} = N^{1 / 2}$ is the rational power of Rational powers $a^{r}$ of a positive base. The factor $\sqrt{N}$ is the price of leaving the convolution unnormalised; it is not an artefact of the proof, and the same factor appears for every pair $(f, g)$ .

Facts & Assumptions

Given: A natural number $N \geq 1$ , functions $f, g \in C^{Z / N}$ , an integer $k$ , and classes $x, y, z \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}$ for every $h \in C^{Z / N}$ (The unitary discrete Fourier transform on $Z / N Z$ ).

[F2]

$(f * g) (x) = \sum_{y \in Z / N} f (y) g (x - y)$ , a single complex number for each class $x$ ; the value depends on classes only (The unnormalised cyclic convolution on $Z / N Z$ ).

[F3]

Finite sums over $Z / N Z$ are computed from any enumeration, are unchanged by reindexing along a bijection, split over disjoint unions and satisfy the finite Fubini rule; scalar factors move through them (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).

[L1]

$\exp (u + v) = \exp u \exp v$ for all complex $u, v$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L2]

Rational powers of the positive real $N$ : $N^{- 1 / 2} N^{1 / 2} = N^{0} = 1$ and the exponent laws hold (Rational powers $a^{r}$ of a positive base, Laws of rational exponents, claims 1 and 2).

[L3]

For fixed $y$ , the map $x \mapsto x - y$ is a bijection of $Z / N Z$ onto itself with inverse $z \mapsto z + y$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold); classes are the objects of $Z / N Z$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[L4]

Field laws of $C$ , in particular associativity and distributivity ( $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.1F1F2F3

Substitute [F2] into [F1] and interchange the two finite sums by the finite Fubini rule [F3]: for the given $k$ , $(F_{N} (f * g)) (k) = N^{- 1 / 2} \sum_{x = 0}^{N - 1} (\sum_{y \in Z / N} f (y) g (x - y)) e^{- 2 π i k x / N} = N^{- 1 / 2} \sum_{y \in Z / N} f (y) \sum_{x \in Z / N} g (x - y) e^{- 2 π i k x / N}$ .

1.2F1F3L1L3L4

Reindex the inner sum and separate the exponentials: for fixed $y$ the substitution $z : = x - y$ is the bijection of [L3], so $\sum_{x} g (x - y) e^{- 2 π i k x / N} = \sum_{z} g (z) e^{- 2 π i k (z + y) / N}$ , and by the addition law [L1] this equals $(\sum_{z} g (z) e^{- 2 π i k z / N}) e^{- 2 π i k y / N} = N^{1 / 2} (F_{N} g) (k) e^{- 2 π i k y / N}$ , the last step by [F1] and [L4].

2.1F1F3L2L4step 1.1step 1.2∎

Inserting step 1.2 into step 1.1 and recognising the remaining sum by [F1], $(F_{N} (f * g)) (k) = N^{- 1 / 2} \sum_{y} f (y) e^{- 2 π i k y / N} N^{1 / 2} (F_{N} g) (k) = N^{- 1 / 2} N^{1 / 2} (F_{N} f) (k) N^{1 / 2} (F_{N} g) (k)$ ; by [L2] the scalar is $N^{- 1 / 2} N^{1 / 2} N^{1 / 2} = N^{1 / 2}$ , so $(F_{N} (f * g)) (k) = N^{1 / 2} (F_{N} f) (k) (F_{N} g) (k)$ as claimed.

Remarks

Comparison with Taylor's convention. Put $h^{#} : = N^{- 1 / 2} F_{N} h$ , so $h^{#}$ carries the forward factor $1 / N$ of Taylor's (11.1). The proved identity gives $(f * g)^{#} = N f^{#} g^{#}$ for the unnormalised convolution here. Taylor's (11.30) instead uses $f ⋆ g : = N^{- 1} (f * g)$ , so $(f ⋆ g)^{#} = f^{#} g^{#}$ by linearity. Both the transform and the convolution normalisations matter.
Cyclic, not linear. The identity computes the cyclic convolution of [F2]. It does not compute the linear convolution of two coefficient sequences unless the length is large enough that no coefficient wraps; the companion page shows the wrap explicitly for two sequences of length two, where the linear coefficient $1$ of $z^{2}$ reappears in degree $0$ .

Depends on

Used by

Cyclic convolution wraps a high coefficient without zero padding Counterexample
Cyclic convolution on ℤ/4ℤ via the DFT Example

Dependency tree · two levels

54 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)