TheoremStatement: 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 chirp-phase error is bounded separately from FFT-convolution error

Statement

Let $N \geq 2$ be prime, $M \geq 2 N - 1$ a power of two, and $K = 2 N - 1$ . Use the Bluestein representation of Bluestein’s chirp identity embeds an arbitrary DFT in a padded cyclic convolution. Suppose every certified chirp phase has absolute error at most $0 < τ \leq 1 / 4$ , $u \leq 1 / 16$ , $E \geq 0$ , the modulation and demodulation products succeed under the six-operation complex model, and the computed cyclic convolution satisfies $∥ \hat{c} - \hat{a} *_{M} \hat{b} ∥_{2} \leq \sqrt{M} E ∥ \hat{a} ∥_{2} ∥ \hat{b} ∥_{2}$ . Put $δ = τ + 3 u (1 + τ)$ and $H = δ (2 + δ) + E (1 + δ)^{2}$ . Then the computed unnormalised length- $N$ DFT output $\hat{X}$ satisfies

∥ \hat{X} - X ∥_{2} \leq \sqrt{M K} [δ + (1 + δ) H] ∥ x ∥_{2} .

The term $δ$ records chirp enclosure and chirp multiplication roundoff; $E$ records the separate FFT, pointwise-product, inverse, and cyclic-convolution scaling error. No mixed-radix stability claim is inferred.

Facts & Assumptions

Given: A prime $N \geq 2$ , $M \geq 2 N - 1$ a power of two, $x \in C^{N}$ , a successful Bluestein computation, and the bounds $τ, u, E$ in the Statement.

[F1]

The exact unnormalised DFT is $X_{k} = γ_{k} (a *_{M} b)_{k}$ , where $a_{j} = α_{j} x_{j}$ , $α_{j} = e^{- π i j^{2} / N}$ , $b_{[t]_{M}} = β_{t} = e^{π i t^{2} / N}$ , and $γ_{k} = e^{- π i k^{2} / N}$ (Bluestein’s chirp identity embeds an arbitrary DFT in a padded cyclic convolution).

[F2]

The certified phase algorithm gives $∣ {\hat{α}}_{j} - α_{j} ∣ \leq τ$ , $∣ {\hat{β}}_{t} - β_{t} ∣ \leq τ$ , and $∣ {\hat{γ}}_{k} - γ_{k} ∣ \leq τ$ ; all exact chirp moduli equal $1$ (Certified phase output encloses the exact unit-circle value, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F3]

A successful complex multiplication contributes at most $3 u ∣ z ∣ ∣ w ∣$ absolute error (Six-operation complex multiplication has a normwise roundoff bound).

[F4]

For length- $M$ vectors, $∥ a *_{M} b ∥_{2} \leq \sqrt{M} ∥ a ∥_{2} ∥ b ∥_{2}$ , and Parseval preserves norms under $F_{M}$ and its inverse (The DFT turns cyclic convolution into a scaled pointwise product, Finite Parseval and Plancherel identity for the unitary DFT, The counting inner product on $C^{Z / N Z}$ ).

[F5]

The computed cyclic convolution satisfies $∥ \hat{c} - \hat{a} *_{M} \hat{b} ∥_{2} \leq \sqrt{M} E ∥ \hat{a} ∥_{2} ∥ \hat{b} ∥_{2}$ (Computed FFT convolution error separates transform, product, inverse, and final-scale terms).

[F6]

For length- $M$ vectors, $∥ u ⊙ v ∥_{2} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ : after squaring, the product $(\sum_{k} ∣ u_{k} ∣^{2}) (\sum_{k} ∣ v_{k} ∣^{2})$ contains the terms $∣ u_{k} ∣^{2} ∣ v_{k} ∣^{2}$ and only additional nonnegative cross terms.

[F7]

The Euclidean norm on $C^{M}$ is subadditive (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors, The counting inner product on $C^{Z / N Z}$ ).

Proof

1.1givenF2F3algebra

Let ${\hat{a}}_{j} = {fl}_{C} ({\hat{α}}_{j} x_{j})$ on $0 \leq j < N$ and zero elsewhere. By [F2]–[F3], $∣ {\hat{a}}_{j} - a_{j} ∣ \leq (τ + 3 u (1 + τ)) ∣ x_{j} ∣ = δ ∣ x_{j} ∣$ , so $∥ \hat{a} - a ∥_{2} \leq δ ∥ x ∥_{2}$ and $∥ \hat{a} ∥_{2} \leq (1 + δ) ∥ x ∥_{2}$ . The vector $b$ has exactly $K$ unit-modulus entries; [F2] gives $∥ \hat{b} - b ∥_{2} \leq τ \sqrt{K} \leq δ \sqrt{K}$ and $∥ \hat{b} ∥_{2} \leq (1 + δ) \sqrt{K}$ .

2.1F1F2F4F5F6F7step 1.1algebra

By bilinearity, $\hat{a} *_{M} \hat{b} - a *_{M} b = (\hat{a} - a) *_{M} \hat{b} + a *_{M} (\hat{b} - b)$ . Applying the exact convolution formula [F4], Parseval, and the pointwise product bound [F6] gives $∥ \hat{a} *_{M} \hat{b} - a *_{M} b ∥_{2} \leq \sqrt{M} (∥ \hat{a} - a ∥_{2} ∥ \hat{b} ∥_{2} + ∥ a ∥_{2} ∥ \hat{b} - b ∥_{2}) \leq \sqrt{M K} δ (2 + δ) ∥ x ∥_{2}$ by step 1.1. The computed-convolution error [F5] is at most $\sqrt{M K} E (1 + δ)^{2} ∥ x ∥_{2}$ . Thus, with $c = a *_{M} b$ and $\hat{c}$ the computed convolution, $∥ \hat{c} - c ∥_{2} \leq \sqrt{M K} H ∥ x ∥_{2}$ ; [F4] and step 1.1 give $∥ c ∥_{2} \leq \sqrt{M K} ∥ x ∥_{2}$ , so $∥ \hat{c} ∥_{2} \leq \sqrt{M K} (1 + H) ∥ x ∥_{2}$ by [F7].

3.1F1F2F3F7step 2.1algebra∎

The output is the componentwise rounded product ${\hat{X}}_{k} = {fl}_{C} ({\hat{γ}}_{k} {\hat{c}}_{k})$ . By [F2]–[F3], $∣ {\hat{X}}_{k} - γ_{k} {\hat{c}}_{k} ∣ \leq δ ∣ {\hat{c}}_{k} ∣$ ; since $∣ γ_{k} ∣ = 1$ , step 2.1 and subadditivity [F7] give $∥ \hat{X} - X ∥_{2} \leq δ ∥ \hat{c} ∥_{2} + ∥ \hat{c} - c ∥_{2} \leq \sqrt{M K} [δ (1 + H) + H] ∥ x ∥_{2} = \sqrt{M K} [δ + (1 + δ) H] ∥ x ∥_{2}$ . This is the claimed separated chirp and convolution bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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

Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., Chapter 24, pp. 452–457 (standard reference, not scraped)
C. Sidney Burrus, Fast Fourier Transforms, Chapter 5 §5.2 (standard reference, not scraped)