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.

Computed FFT convolution error separates transform, product, inverse, and final-scale terms

Statement

Let $M = 2^{q}$ with integer $q \geq 0$ and let $a, b \in C^{M}$ be the arrays actually transformed by Computed FFT cyclic convolution and zero-padded linear convolution (zero-padded in linear mode). Assume all operations succeed, $u \leq 1 / 16$ , the twiddle certificates satisfy $ϵ_{ℓ} \leq ϵ_{t w} \leq 1 / 4$ , and put $η = 10 u + ϵ_{t w}$ , $ρ = (1 + η)^{q} - 1$ , $ϵ_{p} = 3 u$ , $ϵ_{s} = 2 u + u^{2}$ , and $λ = 2 ρ + ρ^{2} + ϵ_{p} (1 + ρ)^{2}$ . If $c = a *_{M} b$ is the exact unnormalised cyclic convolution, then the computed length- $M$ result $\hat{c}$ satisfies

∥ \hat{c} - c ∥_{2} \leq \sqrt{M} [λ + ρ (1 + λ) + ϵ_{s} (1 + ρ) (1 + λ)] ∥ a ∥_{2} ∥ b ∥_{2} .

In linear mode, the same right side bounds the error of the first $n + m - 1$ outputs relative to the exact linear convolution, because zero padding removes cyclic aliasing. This is a conditional error estimate, not an unconditional success certificate.

Facts & Assumptions

Given: The successful computation, length- $M$ input arrays, unitary transforms $A = F_{M} a$ and $B = F_{M} b$ , $u, ϵ_{t w}$ , and the constants in the Statement.

[F1]

The transform and inverse-transform errors satisfy $∥ \hat{A} - A ∥_{2} \leq ρ ∥ a ∥_{2}$ , $∥ \hat{B} - B ∥_{2} \leq ρ ∥ b ∥_{2}$ , and $∥ \hat{z} - F_{M}^{- 1} \hat{p} ∥_{2} \leq ρ ∥ \hat{p} ∥_{2}$ (Computed unitary radix-two FFT has the multiplicative stage error bound, Finite Fourier inversion for the unitary transform on $Z / N Z$ ).

[F2]

For vectors $u, v \in C^{M}$ , $∥ u ⊙ v ∥_{2} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , since $\sum_{k} ∣ u_{k} ∣^{2} ∣ v_{k} ∣^{2} \leq (\sum_{k} ∣ u_{k} ∣^{2}) (\sum_{k} ∣ v_{k} ∣^{2})$ (The counting inner product on $C^{Z / N Z}$ , Real and imaginary parts, complex conjugation, and modulus).

[F3]

Finite Parseval gives $∥ A ∥_{2} = ∥ a ∥_{2}$ , $∥ B ∥_{2} = ∥ b ∥_{2}$ , and $∥ F_{M}^{- 1} z ∥_{2} = ∥ z ∥_{2}$ ; the cyclic convolution identity is $a *_{M} b = \sqrt{M} F_{M}^{- 1} (A ⊙ B)$ (Finite Parseval and Plancherel identity for the unitary DFT, Finite Fourier inversion for the unitary transform on $Z / N Z$ , The DFT turns cyclic convolution into a scaled pointwise product).

[F4]

Each pointwise complex product error is at most $3 u ∣ {\hat{A}}_{k} ∣ ∣ {\hat{B}}_{k} ∣$ (Six-operation complex multiplication has a normwise roundoff bound).

[F5]

Put $s = fl (\sqrt{M})$ . The model gives $∣ s - \sqrt{M} ∣ \leq u \sqrt{M}$ and each componentwise rounded product with $s$ has error at most $u ∣ s z_{j} ∣$ . Thus the combined scale error is at most $[u (1 + u) + u] \sqrt{M} ∥ z ∥_{2} = (2 u + u^{2}) \sqrt{M} ∥ z ∥_{2} = ϵ_{s} \sqrt{M} ∥ z ∥_{2}$ on a successful normal-range result (Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, The standard relative floating-point model and unit roundoff).

[F6]

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

Proof

1.1givenF1F2F3F4algebra

Write $\hat{A} = A + d_{A}$ and $\hat{B} = B + d_{B}$ . By [F1], $∥ d_{A} ∥_{2} \leq ρ ∥ a ∥_{2}$ and $∥ d_{B} ∥_{2} \leq ρ ∥ b ∥_{2}$ , while [F3] gives $∥ A ∥_{2} = ∥ a ∥_{2}$ and $∥ B ∥_{2} = ∥ b ∥_{2}$ . Expand $\hat{A} ⊙ \hat{B} - A ⊙ B = d_{A} ⊙ B + A ⊙ d_{B} + d_{A} ⊙ d_{B}$ . Applying [F2] termwise bounds this transform perturbation by $(2 ρ + ρ^{2}) ∥ a ∥_{2} ∥ b ∥_{2}$ . For the rounded products, [F4] gives coordinate errors $∣ e_{p, k} ∣ \leq ϵ_{p} ∣ {\hat{A}}_{k} ∣ ∣ {\hat{B}}_{k} ∣$ ; squaring and using [F2] yields $∥ e_{p} ∥_{2} \leq ϵ_{p} ∥ \hat{A} ∥_{2} ∥ \hat{B} ∥_{2} \leq ϵ_{p} (1 + ρ)^{2} ∥ a ∥_{2} ∥ b ∥_{2}$ . Thus $∥ \hat{p} - A ⊙ B ∥_{2} \leq λ ∥ a ∥_{2} ∥ b ∥_{2}$ and, by [F2], $∥ \hat{p} ∥_{2} \leq (1 + λ) ∥ a ∥_{2} ∥ b ∥_{2}$ .

2.1step 1.1F1F3F6algebra

Let $z = F_{M}^{- 1} (A ⊙ B) = c / \sqrt{M}$ and let $\hat{z}$ be the computed inverse result before final scaling. By Parseval [F3], $∥ F_{M}^{- 1} (\hat{p} - A ⊙ B) ∥_{2} = ∥ \hat{p} - A ⊙ B ∥_{2}$ ; by the inverse part of [F1], $∥ \hat{z} - F_{M}^{- 1} \hat{p} ∥_{2} \leq ρ ∥ \hat{p} ∥_{2}$ . Subadditivity [F6] and step 1.1 give $∥ \hat{z} - z ∥_{2} \leq [λ + ρ (1 + λ)] ∥ a ∥_{2} ∥ b ∥_{2}$ . Also $∥ \hat{z} ∥_{2} \leq (1 + ρ) ∥ \hat{p} ∥_{2} \leq (1 + ρ) (1 + λ) ∥ a ∥_{2} ∥ b ∥_{2}$ .

3.1step 2.1F5F6algebra∎

The exact scaled target is $\sqrt{M} z = c$ . By [F5], scaling $\hat{z}$ incurs at most $ϵ_{s} \sqrt{M} ∥ \hat{z} ∥_{2}$ additional error. Subadditivity [F6] and step 2.1 therefore give $∥ \hat{c} - c ∥_{2} \leq \sqrt{M} [λ + ρ (1 + λ) + ϵ_{s} (1 + ρ) (1 + λ)] ∥ a ∥_{2} ∥ b ∥_{2}$ , as claimed. In linear mode, Zero padding embeds linear convolution in cyclic convolution without aliasing identifies the exact first $n + m - 1$ cyclic entries with the linear convolution, and coordinate restriction cannot increase the Euclidean norm.

Depends on

Used by

Dependency tree · two levels

49 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 and Problem 24.1, pp. 453–457 (standard reference, not scraped)
C. Sidney Burrus, Fast Fourier Transforms, Chapter 13 §13.1 (standard reference, not scraped)