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 unitary radix-two FFT has the multiplicative stage error bound

Statement

Let $N = 2^{m}$ , $m \geq 0$ , and suppose a successful execution of Computed unitary radix-two FFT with certified twiddle phases has no range failures. If every twiddle certificate satisfies $ϵ_{ℓ} \leq ϵ_{t w} \leq 1 / 4$ and $u \leq 1 / 16$ , put $η = 10 u + ϵ_{t w}$ . Then

∥ {\hat{F}}_{N} x - F_{N} x ∥_{2} \leq ((1 + η)^{m} - 1) ∥ x ∥_{2} .

The conjugated inverse routine has the same bound. If $m η \leq 1$ , the right side is at most $2 m η ∥ x ∥_{2}$ . Thus an $O (u \log N)$ shorthand requires both $ϵ_{t w} = O (u)$ and $u \log N$ small; the theorem makes no such shorthand when twiddle errors are uncontrolled.

Facts & Assumptions

Given: $N = 2^{m}$ , $x \in C^{N}$ , a successful execution, $u \leq 1 / 16$ , and $ϵ_{ℓ} \leq ϵ_{t w} \leq 1 / 4$ for every twiddle certificate.

[F1]

For $N = 2 M$ , split $x$ into even and odd subsequences $e, o$ ; the unnormalised DFT obeys $X_{k} (x) = X_{k} (e) + e^{- 2 π i k / N} X_{k} (o)$ and $X_{k + M} (x) = X_{k} (e) - e^{- 2 π i k / N} X_{k} (o)$ , while $F_{N} = N^{- 1 / 2} X_{N}$ (The radix-two even/odd factorisation of the DFT, The unnormalised engineering DFT and its conversion to the unitary transform, The unitary discrete Fourier transform on $Z / N Z$ ). The recursive FFT computes $X_{N}$ exactly (The recursive radix-two fast Fourier transform, Correctness of the recursive radix-two FFT).

[F2]

Every computed normalized butterfly differs from its exact block by at most $η$ times the pair input norm (A computed unitary radix-two butterfly has error at most (10u + εtw) times its input norm).

[F3]

The unitary DFT preserves the squared Euclidean norm; in particular the exact transforms of the even and odd subsequences have squared norms summing to $∥ x ∥_{2}^{2}$ (Finite Parseval and Plancherel identity for the unitary DFT).

[F4]

Complex conjugation preserves modulus and the Euclidean norm, and the inverse unitary DFT is obtained by conjugating input, applying the forward DFT, and conjugating output (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Finite Fourier inversion for the unitary transform on $Z / N Z$ ).

[F5]

The real exponential is its power series (Real elementary functions and their domains).

[F6]

For $z \in C^{N}$ , $∥ z ∥_{2}^{2} = \sum_{j} ∣ z_{j} ∣^{2}$ (The counting inner product on $C^{Z / N Z}$ ).

[F7]

Every exact twiddle $w = e^{- 2 π i k / N}$ has $∣ w ∣ = 1$ , and $\sqrt{N} = \sqrt{2} \sqrt{N / 2}$ for $N \geq 2$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

Proof

1.1givenF1F7algebrabase

For $m = 0$ , $N = 1$ and the algorithm returns the input exactly, so the error is $0 = (1 + η)^{0} - 1$ . For $m \geq 1$ , [F1] gives the exact unnormalised top outputs $X_{k} (e) + w X_{k} (o)$ and $X_{k} (e) - w X_{k} (o)$ , with $w = e^{- 2 π i k / N}$ . The child unitary outputs are $E_{k} = X_{k} (e) / \sqrt{N / 2}$ and $O_{k} = X_{k} (o) / \sqrt{N / 2}$ ; dividing the parent unnormalised outputs by $\sqrt{N} = \sqrt{2} \sqrt{N / 2}$ gives exactly $U_{w} (E_{k}, O_{k}) = 2^{- 1 / 2} (E_{k} + w O_{k}, E_{k} - w O_{k})$ . By [F7], $∣ w ∣ = 1$ and the scaling identity holds, so the columns of $U_{w}$ have squared norm $1$ and inner product $2^{- 1} (w - w) = 0$ ; hence $U_{w}$ preserves the pair norm.

2.1givenF2F3F6step 1.1algebrainductionih

Suppose the recursive transform of length $N / 2$ has error bound $ρ_{m - 1} = (1 + η)^{m - 1} - 1$ . By [F3] and [F6], stacking the exact even and odd transforms has norm $∥ x ∥_{2}$ ; stacking their computed errors has norm at most $ρ_{m - 1} ∥ x ∥_{2}$ , since the even and odd input coordinates partition $x$ . Hence the stacked computed suboutputs have norm at most $(1 + ρ_{m - 1}) ∥ x ∥_{2}$ . For each $k$ , [F2] bounds the top butterfly error by $η$ times the norm of its computed input pair. Squaring these bounds and summing over $k$ shows that the total top-stage error norm is at most $η (1 + ρ_{m - 1}) ∥ x ∥_{2}$ . The prior subtransform errors contribute at most $ρ_{m - 1} ∥ x ∥_{2}$ through the direct sum of exact norm-preserving blocks in step 1.1. Therefore the total error is at most $[ρ_{m - 1} + η (1 + ρ_{m - 1})] ∥ x ∥_{2} = ((1 + η)^{m} - 1) ∥ x ∥_{2}$ . Induction proves the forward bound for every $m$ .

3.1F4step 2.1

By [F4], the inverse implementation is conjugation before and after the forward routine and conjugation preserves every coordinate modulus. Applying step 2.1 to $\overline{x}$ gives the same error norm for the inverse direction.

4.1givenF5step 2.1algebradischarge-induction: step 2.1∎

If $m η \leq 1$ , then $1 + η \leq e^{η}$ by the power series [F5], so $(1 + η)^{m} \leq e^{m η}$ . For $0 < t \leq 1$ , $e^{t} - 1 = \sum_{j \geq 1} t^{j} / j! \leq t \sum_{j \geq 1} 1 / j! < 2 t$ ; at $t = 0$ , $e^{t} - 1 = 2 t = 0$ . Thus $((1 + η)^{m} - 1) \leq 2 m η$ . If $ϵ_{t w} = O (u)$ , this is $O (m u) = O (u \log_{2} N)$ , with the smallness condition already imposed.

Depends on

Used by

Dependency tree · two levels

78 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, Theorems 24.1–24.2, pp. 452–454 (standard reference, not scraped)
C. Sidney Burrus, Fast Fourier Transforms, Chapter 11 §11.7 (standard reference, not scraped)