LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Bluestein’s chirp identity embeds an arbitrary DFT in a padded cyclic convolution

Statement

Let $N \geq 1$ , $M \geq 2 N - 1$ , and $x \in C^{N}$ . Put $α_{j} = e^{- π i j^{2} / N}$ for $0 \leq j < N$ , $β_{t} = e^{π i t^{2} / N}$ for $- (N - 1) \leq t \leq N - 1$ , and $γ_{k} = e^{- π i k^{2} / N}$ for $0 \leq k < N$ . Embed $a_{j} = α_{j} x_{j}$ for $0 \leq j < N$ and $a_{j} = 0$ otherwise in $C^{M}$ . Embed $b_{[t]_{M}} = β_{t}$ for $- (N - 1) \leq t \leq N - 1$ and set its other entries to zero; this is well-defined because these $2 N - 1$ integers have distinct classes modulo $M$ . Let $c = a *_{M} b$ be the unnormalised cyclic convolution on $Z / M Z$ . Then, for $0 \leq k < N$ ,

(F_{N} x) (k) = N^{- 1 / 2} γ_{k} c_{k},

where $γ_{k} = e^{- π i k^{2} / N}$ . Moreover $c = \sqrt{M} F_{M}^{- 1} ((F_{M} a) ⊙ (F_{M} b))$ , where $⊙$ is coordinatewise multiplication. The identity is exact for every $N$ ; padding to a radix-two $M$ is an implementation choice, not a mathematical restriction.

Facts & Assumptions

Given: Integers $N \geq 1$ , $M \geq 2 N - 1$ , a vector $x \in C^{N}$ , and the definitions of $F_{N}$ , $F_{M}$ , and cyclic convolution.

[F1]

The unnormalised DFT is $X_{k} = \sum_{j = 0}^{N - 1} x_{j} e^{- 2 π i j k / N}$ and $F_{N} x = N^{- 1 / 2} X$ (The unnormalised engineering DFT and its conversion to the unitary transform, The unitary discrete Fourier transform on $Z / N Z$ ).

[F2]

Cyclic convolution is $(a *_{M} b)_{k} = \sum_{j = 0}^{M - 1} a_{j} b_{[k - j]_{M}}$ , and its unitary DFT satisfies $F_{M} (a *_{M} b) = \sqrt{M} (F_{M} a) ⊙ (F_{M} b)$ (The unnormalised cyclic convolution on $Z / N Z$ , The DFT turns cyclic convolution into a scaled pointwise product).

[F3]

The unitary DFT on $Z / M Z$ is invertible with inverse given by the positive-sign unitary DFT (Finite Fourier inversion for the unitary transform on $Z / N Z$ ).

[F4]

The map $t \mapsto [t]_{M}$ is injective on the integer interval $[- (N - 1), N - 1]$ when $M \geq 2 N - 1$ ; complex exponentials satisfy their addition law (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold, 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$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $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})$ ).

[F5]

Positive rational powers satisfy $(r s)^{1 / 2} = r^{1 / 2} s^{1 / 2}$ for positive $r, s$ (Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

Proof

1.1givenF4choose

If two integers $t, t^{'}$ in $[- (N - 1), N - 1]$ have the same class modulo $M$ , then $M$ divides $t - t^{'}$ . But $∣ t - t^{'} ∣ \leq 2 N - 2 < M$ ; the only multiple of $M$ in this range is zero, so $t = t^{'}$ . Thus the definition of $b$ assigns at most one value to each residue. For each $0 \leq k < N$ and $0 \leq j < N$ , the difference $k - j$ lies in $[- (N - 1), N - 1]$ , so the cyclic-convolution sum reduces exactly to $c_{k} = \sum_{j = 0}^{N - 1} α_{j} x_{j} β_{k - j}$ .

2.1step 1.1F1F4algebra

For every such $j, k$ , $- j^{2} + (k - j)^{2} - k^{2} = - 2 k j$ , hence $α_{j} β_{k - j} γ_{k} = e^{- 2 π i j k / N}$ . Summing this identity against $x_{j}$ and using [F1] gives $γ_{k} c_{k} = X_{k}$ and therefore $(F_{N} x) (k) = N^{- 1 / 2} γ_{k} c_{k}$ .

3.1F2F3F5algebra∎

Applying [F2] to $a, b$ gives $F_{M} c = \sqrt{M} ((F_{M} a) ⊙ (F_{M} b))$ . Applying the positive-sign inverse in [F3] and pulling the scalar $\sqrt{M}$ through its finite sum gives $c = \sqrt{M} F_{M}^{- 1} ((F_{M} a) ⊙ (F_{M} b))$ , as claimed.

Depends on

Used by

Dependency tree · two levels

61 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

C. Sidney Burrus, Fast Fourier Transforms, Chapter 5 §5.2, equations (5.15)–(5.17) (standard reference, not scraped)