Fast Fourier transform

DefinitionDiscrete Fourier sum#✓fully proved

For a natural number \(N\), a complex number \(\omega\), a sequence \(f : \mathbb{N} \to \mathbb{C}\) and a natural number \(k\), the unnormalized discrete Fourier sum of length \(N\) at frequency \(k\) is \(\sum_{j=0}^{N-1} \omega^{jk} f(j)\).

No condition is placed on \(\omega\); the usual DFT takes \(\omega = e^{-2\pi i/N}\).

def dftSum (N : ℕ) (ω : ℂ) (f : ℕ → ℂ) (k : ℕ) : ℂ :=
  ∑ j ∈ Finset.range N, ω ^ (j * k) * f j

Used by 11

Used byRadix-2 Cooley–Tukey splitting · The DFT sum at a root of unity depends only on the frequency modulo the length · Even–odd splitting of the DFT sum · The array FFT computes the discrete Fourier transform · Conjugating around the FFT conjugates the root · Correctness of the radix-two FFT · The radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · The radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Correctness of the inverse FFT · Inverse FFT at the negative-sign root computes the inverse DFT · Inverse FFT at the positive-sign root computes the normalized forward DFT

TheoremEven–odd splitting of the DFT sum#✓fully proved

For every natural number \(n\), every \(\omega \in \mathbb{C}\), every \(f : \mathbb{N} \to \mathbb{C}\) and every natural number \(K\),

\[\sum_{j < 2n} \omega^{jK} f(j) = \sum_{t < n} (\omega^2)^{tK} f(2t) + \omega^K \sum_{t < n} (\omega^2)^{tK} f(2t + 1).\]

public theorem dftSum_two_mul (n : ℕ) (ω : ℂ) (f : ℕ → ℂ) (K : ℕ) :
    dftSum (2 * n) ω f K =
      dftSum n (ω ^ 2) (fun t => f (2 * t)) K +
        ω ^ K * dftSum n (ω ^ 2) (fun t => f (2 * t + 1)) K

Uses 1 · Used by 1

Statement usesDiscrete Fourier sum

Used byRadix-2 Cooley–Tukey splitting

TheoremThe DFT sum at a root of unity depends only on the frequency modulo the length#✓fully proved

Let \(n\) be a natural number and let \(\omega \in \mathbb{C}\) satisfy \(\omega^n = 1\). Then for every \(f : \mathbb{N} \to \mathbb{C}\) and every natural number \(K\), the discrete Fourier sum of length \(n\) at frequency \(K\) equals the one at frequency \(K \bmod n\):

\[\sum_{j < n} \omega^{jK} f(j) = \sum_{j < n} \omega^{j (K \bmod n)} f(j),\]

where \(K \bmod n\) is the remainder of \(K\) on division by \(n\) (with \(K \bmod 0 = K\)).

public theorem dftSum_mod (n : ℕ) (ω : ℂ) (hω : ω ^ n = 1) (f : ℕ → ℂ) (K : ℕ) :
    dftSum n ω f K = dftSum n ω f (K % n)

Uses 1 · Used by 1

Statement usesDiscrete Fourier sum

Used byRadix-2 Cooley–Tukey splitting

TheoremRadix-2 Cooley–Tukey splitting#✓fully proved

For \(\omega \in \mathbb{C}\), \(f : \mathbb{N} \to \mathbb{C}\) and natural numbers \(N\) and \(k\), write \(D_N(\omega, f, k) = \sum_{j < N} \omega^{jk} f(j)\) for the discrete Fourier sum. Let \(n\) be a natural number and let \(\omega \in \mathbb{C}\) satisfy \(\omega^{2n} = 1\). Then for every \(f : \mathbb{N} \to \mathbb{C}\) and every natural number \(K\),

\[D_{2n}(\omega, f, K) = D_n(\omega^2, f_0, K \bmod n) + \omega^K D_n(\omega^2, f_1, K \bmod n),\]

where \(f_0(t) = f(2t)\), \(f_1(t) = f(2t + 1)\), and \(K \bmod n\) is the remainder of \(K\) on division by \(n\) (with \(K \bmod 0 = K\)). So a length-\(2n\) transform is two length-\(n\) transforms on the even and odd samples, combined with the twiddle factor \(\omega^K\).

Proof: Split the range into even and odd indices, rewrite the powers, and use root-of-unity periodicity to reduce the frequency modulo \(n\), as in the section "The radix-2 DIT case" of Wikipedia, "Cooley–Tukey FFT algorithm".

public theorem cooley_tukey (n : ℕ) (ω : ℂ) (hω : ω ^ (2 * n) = 1)
    (f : ℕ → ℂ) (K : ℕ) :
    dftSum (2 * n) ω f K =
      dftSum n (ω ^ 2) (fun t => f (2 * t)) (K % n) +
        ω ^ K * dftSum n (ω ^ 2) (fun t => f (2 * t + 1)) (K % n)

Sources

• J. W. Cooley and J. W. Tukey, Math. Comp. 19 (1965) (decimation in time).

Uses 3 · Used by 1

Statement usesDiscrete Fourier sum

Proof usesThe DFT sum at a root of unity depends only on the frequency modulo the length · Even–odd splitting of the DFT sum

Used byCorrectness of the radix-two FFT

DefinitionFFT operation count#✓fully proved

For a natural number \(n\), the closed-form FFT operation count is \(n \lfloor \log_2 n \rfloor\), where \(\lfloor \log_2 n \rfloor\) is the largest \(m\) with \(2^m \le n\) (taken to be \(0\) when \(n = 0\)).

def fftCost (n : ℕ) : ℕ :=
  n * Nat.log 2 n

Used by 1

Used byThe FFT cost satisfies the radix-2 recurrence

TheoremThe FFT cost satisfies the radix-2 recurrence#✓fully proved

Let \(C(n) = n \lfloor \log_2 n \rfloor\) be the closed-form FFT operation count. For every natural number \(n > 0\), \(C(2n) = 2\,C(n) + 2n\).

Proof: Since \(n > 0\), \(\lfloor \log_2 (2n) \rfloor = \lfloor \log_2 n \rfloor + 1\); expand the product.

public theorem fftCost_recurrence (n : ℕ) (hn : 0 < n) :
    fftCost (2 * n) = 2 * fftCost n + 2 * n

Sources

• J. W. Cooley and J. W. Tukey, Math. Comp. 19 (1965) (n log n operation count).

Uses 1

Statement usesFFT operation count

DefinitionEven–odd split for the FFT#✓fully proved

For a commutative ring \(R\), a natural number \(m\) and a vector \(x = (x_0, \dots, x_{2m-1}) \in R^{2m}\), the split returns the pair of vectors \((x_0, x_2, \dots, x_{2m-2})\) and \((x_1, x_3, \dots, x_{2m-1})\) in \(R^m\) of the entries of \(x\) at even and at odd indices, in order, at a time cost of \(4m\) (the charged reads and writes).

def fftSplit {m : Nat} (xs : Vector R (m * 2)) :
    TimeM Nat (Vector R m × Vector R m) :=
  let even := Vector.ofFn fun i : Fin m =>
    xs[2 * i.val]'(by have hi := i.isLt; omega)
  let odd := Vector.ofFn fun i : Fin m =>
    xs[2 * i.val + 1]'(by have hi := i.isLt; omega)
  ⟨(even, odd), 4 * m⟩

Used by 8

Used byRadix-two fast Fourier transform · Correctness of the radix-two FFT · High half of the FFT butterfly recurrence · Low half of the FFT butterfly recurrence · The FFT split extracts the even-indexed entries · The FFT split extracts the odd-indexed entries · Cost of the FFT even/odd split · Exact cost of the radix-two FFT

DefinitionOne FFT butterfly#✓fully proved

For a commutative ring \(R\), an element \(\omega \in R\), vectors \(q, r \in R^m\), a state \((w, y)\) with \(w \in R\) and \(y \in R^{2m}\), and an index \(k < m\), the butterfly at \(k\) returns the state \((w \omega, y')\), where \(y'\) is obtained from \(y\) by setting entry \(k\) to \(q_k + w r_k\) and entry \(k + m\) to \(q_k - w r_k\), at a time cost of \(8\).

def fftButterfly {m : Nat} (omega : R) (q r : Vector R m)
    (state : R × Vector R (m * 2)) (k : Fin m) :
    TimeM Nat (R × Vector R (m * 2)) :=
  let (w, out) := state
  let a := q[k.val]
  let b := r[k.val]
  let t := w * b
  let low := out.set k.val (a + t) (by have hk := k.isLt; omega)
  let both := low.set (k.val + m) (a - t) (by have hk := k.isLt; omega)
  ⟨(w * omega, both), 8⟩

Used by 7

Used byFFT butterfly pass · Result of the butterfly loop · Cost of the FFT butterfly pass · Upper write of a butterfly step · Lower write of a butterfly step · A butterfly step leaves other entries unchanged · Cost of one FFT butterfly

DefinitionFFT butterfly pass#✓fully proved

For a commutative ring \(R\), an element \(\omega \in R\) and vectors \(q, r \in R^m\) and \(y \in R^{2m}\), the butterfly pass starts from the state \((1, y)\), applies the FFT butterfly with \(\omega\), \(q\) and \(r\) at the indices \(k = 0, 1, \dots, m - 1\) in increasing order, and returns the final state; its time cost is the sum of the costs of these \(m\) butterflies.

def fftButterflies {m : Nat} (omega : R) (q r : Vector R m)
    (out : Vector R (m * 2)) : TimeM Nat (R × Vector R (m * 2)) :=
  (List.finRange m).foldlM (fftButterfly omega q r) (1, out)

Uses 1 · Used by 6

Statement usesOne FFT butterfly

Used byRadix-two fast Fourier transform · Result of the butterfly loop · Cost of the FFT butterfly pass · High half of the FFT butterfly recurrence · Low half of the FFT butterfly recurrence · Exact cost of the radix-two FFT

DefinitionRadix-two fast Fourier transform#✓fully proved

For a commutative ring \(R\), a natural number \(d\), an element \(\omega \in R\) and a vector \(x \in R^{2^d}\), the FFT of \(x\) with root \(\omega\) is defined by recursion on \(d\). For \(d = 0\) it returns \(x\) at cost \(0\). For \(d + 1\) it splits \(x\) into its even- and odd-indexed subvectors \(e, o \in R^{2^d}\) (cost \(4 \cdot 2^d\)), computes \(\omega^2\) (cost \(1\)), computes the FFTs \(q\) of \(e\) and \(r\) of \(o\) with root \(\omega^2\), writes a zero vector \(y \in R^{2^{d+1}}\) (cost \(2^{d+1}\)), and returns the vector part of the result of the butterfly pass with \(\omega\), \(q\) and \(r\) on \(y\). Its time cost is the sum of the costs of all these steps.

The two transformed halves are stored once and combined with a running twiddle factor. No assumption on \(\omega\) is needed to run the algorithm; one is needed only for its correctness.

def fft : (d : Nat) → R → Vector R (2 ^ d) → TimeM Nat (Vector R (2 ^ d))
  | 0, _, xs => pure xs
  | d + 1, omega, xs => do
      let halves ← fftSplit xs
      let square ← (⟨omega * omega, 1⟩ : TimeM Nat R)
      let q ← fft d square halves.1
      let r ← fft d square halves.2
      let out ← (⟨Vector.replicate (2 ^ d * 2) 0, 2 ^ d * 2⟩ :
        TimeM Nat (Vector R (2 ^ d * 2)))
      let combined ← fftButterflies omega q r out
      pure combined.2

Uses 2 · Used by 30

Statement usesFFT butterfly pass · Even–odd split for the FFT

Used byRadix-two FFT on arrays · The array FFT computes the discrete Fourier transform · The array FFT rejects exactly the non-powers of two · The array FFT agrees with the vector FFT · Exact cost of the array FFT · The array FFT costs the same as the vector FFT · FFT circular convolution · Output of FFT circular convolution · FFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · Exact cost of FFT circular convolution · Conjugating around the FFT conjugates the root · Correctness of the radix-two FFT · FFT after inverse FFT is the identity at the negative-sign root · FFT after inverse FFT at the positive root is the identity · High half of the FFT butterfly recurrence · Low half of the FFT butterfly recurrence · The FFT of depth zero returns its input · The radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · The radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Exact cost of the radix-two FFT · Exact cost of the radix-two FFT in terms of the input length · Cost bound for the radix-two FFT · Inverse FFT by conjugation · Correctness of the inverse FFT · Inverse FFT after FFT is the identity at the negative-sign root · Inverse FFT after FFT at the positive root is the identity · The inverse FFT is a normalized FFT at the conjugate root · Exact operation count of the inverse FFT · Operation bound for the inverse FFT

DefinitionRadix-two FFT on arrays#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\) and \(x\) an array over \(R\) of length \(n\), and let \(d = \lfloor \log_2 n \rfloor\) (with \(d = 0\) when \(n = 0\)). If \(n = 2^d\), the array FFT runs the radix-two FFT with root \(\omega\) on \(x\), viewed as a vector of length \(2^d\), and returns its output as an array, with the cost of that run. Otherwise it returns no result, at cost \(0\); the length check itself is free.

def fftArray (omega : R) (xs : Array R) : TimeM Nat (Option (Array R)) :=
  if h : xs.size = 2 ^ xs.size.log2 then
    TimeM.bind (fft xs.size.log2 omega ⟨xs, h⟩) fun out => pure (some out.toArray)
  else
    pure none

Uses 1 · Used by 5

Statement usesRadix-two fast Fourier transform

Used byThe array FFT computes the discrete Fourier transform · The array FFT rejects exactly the non-powers of two · The array FFT agrees with the vector FFT · Exact cost of the array FFT · The array FFT costs the same as the vector FFT

TheoremThe array FFT rejects exactly the non-powers of two#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\) and \(x\) an array over \(R\). The array FFT of \(x\) with root \(\omega\) returns no result if and only if the length of \(x\) is different from \(2^d\) for every natural number \(d\).

In particular the empty array is rejected and an array of length \(1 = 2^0\) is accepted.

theorem fftArray_eq_none_iff (omega : R) (xs : Array R) :
    (fftArray omega xs).ret = none ↔ ∀ d : Nat, xs.size ≠ 2 ^ d

Uses 2

Statement usesRadix-two FFT on arrays

Proof usesRadix-two fast Fourier transform

TheoremLower write of a butterfly step#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\), \(m\) a natural number, \(q, r\) vectors over \(R\) of length \(m\), \(w \in R\) a twiddle, \(o\) an output vector over \(R\) of length \(2m\), and \(k < m\). Then the butterfly step at index \(k\) applied to the state \((w, o)\) produces an output vector whose entry at index \(k\) is \(q_k + w r_k\).

theorem fftButterfly_ret_low {m : Nat} (omega : R) (q r : Vector R m)
    (state : R × Vector R (m * 2)) (k : Fin m) :
    (fftButterfly omega q r state k).ret.2[k.val]'(by have h := k.isLt; omega) =
      q[k.val] + state.1 * r[k.val]

Uses 1 · Used by 1

Statement usesOne FFT butterfly

Used byResult of the butterfly loop

TheoremUpper write of a butterfly step#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\), \(m\) a natural number, \(q, r\) vectors over \(R\) of length \(m\), \(w \in R\) a twiddle, \(o\) an output vector over \(R\) of length \(2m\), and \(k < m\). Then the butterfly step at index \(k\) applied to the state \((w, o)\) produces an output vector whose entry at index \(k + m\) is \(q_k - w r_k\).

theorem fftButterfly_ret_high {m : Nat} (omega : R) (q r : Vector R m)
    (state : R × Vector R (m * 2)) (k : Fin m) :
    (fftButterfly omega q r state k).ret.2[k.val + m]'(by have h := k.isLt; omega) =
      q[k.val] - state.1 * r[k.val]

Uses 1 · Used by 1

Statement usesOne FFT butterfly

Used byResult of the butterfly loop

TheoremA butterfly step leaves other entries unchanged#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\), \(m\) a natural number, \(q, r\) vectors over \(R\) of length \(m\), \(w \in R\) a twiddle, \(o\) an output vector over \(R\) of length \(2m\), and \(k < m\). Then for every index \(i < 2m\) with \(i \ne k\) and \(i \ne k + m\), the butterfly step at index \(k\) applied to the state \((w, o)\) produces an output vector whose entry at index \(i\) is \(o_i\).

theorem fftButterfly_ret_other {m : Nat} (omega : R) (q r : Vector R m)
    (state : R × Vector R (m * 2)) (k : Fin m) (i : Fin (m * 2))
    (hlo : i.val ≠ k.val) (hhi : i.val ≠ k.val + m) :
    (fftButterfly omega q r state k).ret.2[i.val] = state.2[i.val]

Uses 1 · Used by 1

Statement usesOne FFT butterfly

Used byResult of the butterfly loop

TheoremResult of the butterfly loop#✓fully proved

Let \(R\) be a commutative ring, \(\omega \in R\), \(m\) a natural number, \(q = (q_0, \dots, q_{m-1})\) and \(r = (r_0, \dots, r_{m-1})\) vectors over \(R\), and \(o\) a vector over \(R\) of length \(2m\). The butterfly loop with root \(\omega\) on \(q\) and \(r\), started from twiddle \(1\) and output vector \(o\), ends with twiddle \(\omega^m\) and an output vector \(y\) such that \(y_k = q_k + \omega^k r_k\) and \(y_{k+m} = q_k - \omega^k r_k\) for every \(k < m\).

theorem fftButterflies_ret {m : Nat} (omega : R) (q r : Vector R m)
    (out : Vector R (m * 2)) :
    (fftButterflies omega q r out).ret.1 = omega ^ m ∧ ∀ k : Fin m,
      (fftButterflies omega q r out).ret.2[k.val]'(by have h := k.isLt; omega) =
        q[k.val] + omega ^ k.val * r[k.val] ∧
      (fftButterflies omega q r out).ret.2[k.val + m]'(by have h := k.isLt; omega) =
        q[k.val] - omega ^ k.val * r[k.val]

Uses 5 · Used by 2

Statement usesFFT butterfly pass

Proof usesOne FFT butterfly · Upper write of a butterfly step · Lower write of a butterfly step · A butterfly step leaves other entries unchanged

Used byHigh half of the FFT butterfly recurrence · Low half of the FFT butterfly recurrence

TheoremThe FFT split extracts the even-indexed entries#✓fully proved

Let \(R\) be a type, \(m\) a natural number and \(x = (x_0, \dots, x_{2m-1})\) a vector of length \(2m\) over \(R\). For every \(k < m\), entry \(k\) of the first (even) vector returned by the FFT split of \(x\) is \(x_{2k}\).

theorem fftSplit_ret_even {m : Nat} (xs : Vector R (m * 2)) (k : Fin m) :
    (fftSplit xs).ret.1[k.val] = xs[2 * k.val]'(by have h := k.isLt; omega)

Uses 1 · Used by 1

Statement usesEven–odd split for the FFT

Used byCorrectness of the radix-two FFT

TheoremThe FFT split extracts the odd-indexed entries#✓fully proved

Let \(R\) be a type, \(m\) a natural number and \(x = (x_0, \dots, x_{2m-1})\) a vector of length \(2m\) over \(R\). For every \(k < m\), entry \(k\) of the second (odd) vector returned by the FFT split of \(x\) is \(x_{2k+1}\).

theorem fftSplit_ret_odd {m : Nat} (xs : Vector R (m * 2)) (k : Fin m) :
    (fftSplit xs).ret.2[k.val] = xs[2 * k.val + 1]'(by have h := k.isLt; omega)

Uses 1 · Used by 1

Statement usesEven–odd split for the FFT

Used byCorrectness of the radix-two FFT

TheoremThe FFT of depth zero returns its input#✓fully proved

Let \(R\) be a commutative ring. For every \(\omega \in R\) and every vector \(x \in R^{2^0}\), the vector returned by the radix-two FFT of depth \(0\) with root \(\omega\) on \(x\) is \(x\) itself.

theorem fft_ret_zero (omega : R) (xs : Vector R (2 ^ 0)) :
    (fft 0 omega xs).ret = xs

Uses 1 · Used by 1

Statement usesRadix-two fast Fourier transform

Used byCorrectness of the radix-two FFT

TheoremLow half of the FFT butterfly recurrence#✓fully proved

Let \(R\) be a commutative ring, \(d\) a natural number, \(\omega \in R\) and \(x \in R^{2^{d+1}}\), with entries indexed from \(0\). Let \(e, o \in R^{2^d}\) be the even- and odd-indexed subsequences of \(x\) returned by the FFT split, and let \(E\) and \(O\) be the vectors returned by the radix-two FFT of depth \(d\) with root \(\omega \cdot \omega\) on \(e\) and on \(o\). Then for every \(k < 2^d\), entry \(k\) of the vector returned by the radix-two FFT of depth \(d + 1\) with root \(\omega\) on \(x\) equals \(E_k + \omega^k O_k\).

theorem fft_ret_succ_low (d : Nat) (omega : R) (xs : Vector R (2 ^ (d + 1)))
    (k : Fin (2 ^ d)) :
    (fft (d + 1) omega xs).ret[k.val]'(by have h := k.isLt; simp only [pow_succ]; omega) =
      (fft d (omega * omega) (fftSplit xs).ret.1).ret[k.val] +
        omega ^ k.val * (fft d (omega * omega) (fftSplit xs).ret.2).ret[k.val]

Uses 4 · Used by 1

Statement usesRadix-two fast Fourier transform · Even–odd split for the FFT

Proof usesFFT butterfly pass · Result of the butterfly loop

Used byCorrectness of the radix-two FFT

TheoremHigh half of the FFT butterfly recurrence#✓fully proved

Let \(R\) be a commutative ring, \(d\) a natural number, \(\omega \in R\) and \(x \in R^{2^{d+1}}\), with entries indexed from \(0\). Let \(e, o \in R^{2^d}\) be the even- and odd-indexed subsequences of \(x\) returned by the FFT split, and let \(E\) and \(O\) be the vectors returned by the radix-two FFT of depth \(d\) with root \(\omega \cdot \omega\) on \(e\) and on \(o\). Then for every \(k < 2^d\), entry \(k + 2^d\) of the vector returned by the radix-two FFT of depth \(d + 1\) with root \(\omega\) on \(x\) equals \(E_k - \omega^k O_k\).

theorem fft_ret_succ_high (d : Nat) (omega : R) (xs : Vector R (2 ^ (d + 1)))
    (k : Fin (2 ^ d)) :
    (fft (d + 1) omega xs).ret[k.val + 2 ^ d]'
        (by have h := k.isLt; simp only [pow_succ]; omega) =
      (fft d (omega * omega) (fftSplit xs).ret.1).ret[k.val] -
        omega ^ k.val * (fft d (omega * omega) (fftSplit xs).ret.2).ret[k.val]

Uses 4 · Used by 1

Statement usesRadix-two fast Fourier transform · Even–odd split for the FFT

Proof usesFFT butterfly pass · Result of the butterfly loop

Used byCorrectness of the radix-two FFT

TheoremCost of the FFT even/odd split#✓fully proved

For every natural number \(m\) and every vector \(x\) of length \(2m\), splitting \(x\) into its even-indexed and its odd-indexed subsequences costs exactly \(4m\) charged operations: two reads and two writes for each of the \(m\) even/odd pairs.

@[simp] theorem fftSplit_time {m : Nat} (xs : Vector R (m * 2)) :
    (fftSplit xs).time = 4 * m

Uses 1 · Used by 1

Statement usesEven–odd split for the FFT

Used byExact cost of the radix-two FFT

TheoremCost of one FFT butterfly#✓fully proved

Let \(R\) be a commutative ring and \(m\) a natural number. For every \(\omega \in R\), all vectors \(q, r \in R^m\), every current twiddle \(w \in R\) and output vector of length \(2m\) over \(R\), and every index \(k < m\), one butterfly step costs exactly \(8\) charged operations: two reads, four scalar operations and two writes.

@[simp] theorem fftButterfly_time {m : Nat} (omega : R) (q r : Vector R m)
    (state : R × Vector R (m * 2)) (k : Fin m) :
    (fftButterfly omega q r state k).time = 8

Uses 1 · Used by 1

Statement usesOne FFT butterfly

Used byCost of the FFT butterfly pass

TheoremCost of the FFT butterfly pass#✓fully proved

Let \(R\) be a commutative ring and \(m\) a natural number. For every \(\omega \in R\), all vectors \(q, r \in R^m\) and every output vector of length \(2m\) over \(R\), the pass that, starting from twiddle \(1\), applies one butterfly for each index \(k < m\) in increasing order costs exactly \(8m\) charged operations.

theorem fftButterflies_time {m : Nat} (omega : R) (q r : Vector R m)
    (out : Vector R (m * 2)) :
    (fftButterflies omega q r out).time = 8 * m

Uses 3 · Used by 1

Statement usesFFT butterfly pass

Proof usesOne FFT butterfly · Cost of one FFT butterfly

Used byExact cost of the radix-two FFT

TheoremExact cost of the radix-two FFT#✓fully proved

Let \(R\) be a commutative ring. For every natural number \(d\), every \(\omega \in R\) and every vector \(x \in R^{2^d}\), the radix-two FFT of \(x\) with root \(\omega\) costs \(T\) charged operations, where \(T + 1 = (7d + 1) \cdot 2^d\); that is, \(T = (7d + 1) \cdot 2^d - 1\).

The count includes the charged reads and writes of the even/odd splits and the writes that initialize each output vector.

theorem fft_time_add_one (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fft d omega xs).time + 1 = (7 * d + 1) * 2 ^ d

Uses 5 · Used by 5

Statement usesRadix-two fast Fourier transform

Proof usesFFT butterfly pass · Cost of the FFT butterfly pass · Even–odd split for the FFT · Cost of the FFT even/odd split

Used byExact cost of the array FFT · Exact cost of FFT circular convolution · Exact cost of the radix-two FFT in terms of the input length · Cost bound for the radix-two FFT · Exact operation count of the inverse FFT

TheoremExact cost of the radix-two FFT in terms of the input length#✓fully proved

Let \(R\) be a commutative ring. For every natural number \(d\), every \(\omega \in R\) and every vector \(x\) over \(R\) of length \(n = 2^d\), the radix-two FFT of \(x\) with root \(\omega\) costs \(T\) charged operations, where \(T + 1 = (7 \log_2 n + 1) \cdot n\).

theorem fft_time_add_one_log2 (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fft d omega xs).time + 1 = (7 * Nat.log2 (2 ^ d) + 1) * 2 ^ d

Uses 2

Statement usesRadix-two fast Fourier transform

Proof usesExact cost of the radix-two FFT

TheoremCost bound for the radix-two FFT#✓fully proved

Let \(R\) be a commutative ring. For every natural number \(d\), every \(\omega \in R\) and every vector \(x \in R^{2^d}\), the radix-two FFT of \(x\) with root \(\omega\) costs at most \(8 \cdot 2^d \cdot d\) charged operations, that is, at most eight per entry per recursion level.

theorem fft_time_le (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fft d omega xs).time ≤ 8 * (2 ^ d) * d

Uses 2 · Used by 1

Statement usesRadix-two fast Fourier transform

Proof usesExact cost of the radix-two FFT

Used byOperation bound for the inverse FFT

TheoremCorrectness of the radix-two FFT#✓fully proved

For every natural number \(d\), every primitive \(2^d\)-th root of unity \(\omega \in \mathbb{C}\), every vector \(x = (x_0, \dots, x_{2^d - 1})\) in \(\mathbb{C}^{2^d}\) and every \(k < 2^d\), the \(k\)-th entry of the radix-two FFT of \(x\) with root \(\omega\) equals the discrete Fourier sum \(\sum_{j=0}^{2^d - 1} \omega^{jk} x_j\).

theorem fft_correct (d : Nat) (omega : ℂ) (hroot : IsPrimitiveRoot omega (2 ^ d))
    (xs : Vector ℂ (2 ^ d)) (k : Fin (2 ^ d)) :
    (fft d omega xs).ret[k.val] =
      dftSum (2 ^ d) omega (fun j => xs.toArray.getD j 0) k.val

Uses 9 · Used by 5

Statement usesRadix-two fast Fourier transform · Discrete Fourier sum

Proof usesEven–odd split for the FFT · The FFT split extracts the even-indexed entries · The FFT split extracts the odd-indexed entries · High half of the FFT butterfly recurrence · Low half of the FFT butterfly recurrence · The FFT of depth zero returns its input · Radix-2 Cooley–Tukey splitting

Used byThe array FFT computes the discrete Fourier transform · Conjugating around the FFT conjugates the root · The radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · The radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Correctness of the inverse FFT

TheoremThe array FFT agrees with the vector FFT#✓fully proved

Let \(R\) be a commutative ring, \(d\) a natural number, \(\omega \in R\) and \(x\) a vector over \(R\) of length \(2^d\). Then the array FFT of \(x\), viewed as an array, with root \(\omega\) returns a result, namely the output of the radix-two FFT of the length-\(2^d\) vector \(x\) with root \(\omega\), viewed as an array.

theorem fftArray_ret_of_vector {R : Type u} [CommRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fftArray omega xs.toArray).ret = some (fft d omega xs).ret.toArray

Uses 2 · Used by 1

Statement usesRadix-two fast Fourier transform · Radix-two FFT on arrays

Used byThe array FFT computes the discrete Fourier transform

TheoremThe array FFT costs the same as the vector FFT#✓fully proved

Let \(R\) be a commutative ring, \(d\) a natural number, \(\omega \in R\) and \(x\) a vector over \(R\) of length \(2^d\). Then the cost of the array FFT of \(x\), viewed as an array, with root \(\omega\) equals the cost of the radix-two FFT of the length-\(2^d\) vector \(x\) with root \(\omega\).

theorem fftArray_time_of_vector {R : Type u} [CommRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fftArray omega xs.toArray).time = (fft d omega xs).time

Uses 2 · Used by 1

Statement usesRadix-two fast Fourier transform · Radix-two FFT on arrays

Used byExact cost of the array FFT

TheoremThe array FFT computes the discrete Fourier transform#✓fully proved

Let \(d\) be a natural number, \(\omega \in \mathbb{C}\) a primitive \(2^d\)-th root of unity, \(x_0, \dots, x_{2^d - 1}\) complex numbers and \(k < 2^d\). Then the array FFT of the array \((x_0, \dots, x_{2^d - 1})\) with root \(\omega\) returns an array \(y\) of length \(2^d\) whose entry at index \(k\) is the discrete Fourier sum \(\sum_{j=0}^{2^d - 1} \omega^{jk} x_j\).

theorem fftArray_correct (d : Nat) (omega : ℂ)
    (hroot : IsPrimitiveRoot omega (2 ^ d)) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    ∃ ys : Array ℂ, (fftArray omega xs.toArray).ret = some ys ∧
      ys.size = 2 ^ d ∧
      ys.getD k.val 0 =
        MathlibExt.Analysis.Fourier.FastFourierTransformWanted.dftSum
          (2 ^ d) omega (fun j => xs.toArray.getD j 0) k.val

Uses 5

Statement usesRadix-two FFT on arrays · Discrete Fourier sum

Proof usesRadix-two fast Fourier transform · The array FFT agrees with the vector FFT · Correctness of the radix-two FFT

TheoremExact cost of the array FFT#✓fully proved

Let \(R\) be a commutative ring, \(d\) a natural number, \(\omega \in R\) and \(x\) a vector over \(R\) of length \(2^d\). Then the cost \(T\) of the array FFT of \(x\), viewed as an array, with root \(\omega\) satisfies \(T + 1 = (7d + 1) \cdot 2^d\).

Costs are counted in the scalar-operation and array-access model of the radix-two FFT.

theorem fftArray_time_add_one {R : Type u} [CommRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (fftArray omega xs.toArray).time + 1 = (7 * d + 1) * 2 ^ d

Uses 4

Statement usesRadix-two FFT on arrays

Proof usesRadix-two fast Fourier transform · The array FFT costs the same as the vector FFT · Exact cost of the radix-two FFT

TheoremThe radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT#✓fully proved

Let \(n = 2^d\) and let \(x_0, \dots, x_{n-1}\) be complex numbers, indexed by \(\mathbb{Z}/n\mathbb{Z}\). Run the radix-two FFT on \(x\) with sample root \(\omega = e^{-2\pi i/n}\), the value at \(-1\) of the standard additive character of \(\mathbb{Z}/n\mathbb{Z}\). Then for every \(k < n\), entry \(k\) of the returned vector equals the discrete Fourier transform coefficient \(\sum_{j \in \mathbb{Z}/n\mathbb{Z}} e^{-2\pi i jk/n} x_j\).

theorem fft_stdAddChar_neg_one (d : Nat) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (fft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d))) xs).ret[k.val] =
      ZMod.dft (fun j : ZMod (2 ^ d) => xs.toArray.getD j.val 0)
        (k.val : ZMod (2 ^ d))

Uses 3 · Used by 3

Statement usesRadix-two fast Fourier transform

Proof usesCorrectness of the radix-two FFT · Discrete Fourier sum

Used byFFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT after inverse FFT is the identity at the negative-sign root · Inverse FFT after FFT is the identity at the negative-sign root

TheoremThe radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT#✓fully proved

Let \(n = 2^d\) and let \(x_0, \dots, x_{n-1}\) be complex numbers, indexed by \(\mathbb{Z}/n\mathbb{Z}\). Run the radix-two FFT on \(x\) with sample root \(\omega = e^{2\pi i/n}\), the value at \(1\) of the standard additive character of \(\mathbb{Z}/n\mathbb{Z}\). Then for every \(k < n\), entry \(k\) of the returned vector multiplied by \(1/n\) equals the inverse discrete Fourier transform coefficient \(\frac{1}{n} \sum_{j \in \mathbb{Z}/n\mathbb{Z}} e^{2\pi i jk/n} x_j\).

theorem fft_stdAddChar_one_normalized (d : Nat) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (2 ^ d : ℂ)⁻¹ * (fft d (ZMod.stdAddChar (1 : ZMod (2 ^ d))) xs).ret[k.val] =
      ZMod.dft.symm (fun j : ZMod (2 ^ d) => xs.toArray.getD j.val 0)
        (k.val : ZMod (2 ^ d))

Uses 3 · Used by 3

Statement usesRadix-two fast Fourier transform

Proof usesCorrectness of the radix-two FFT · Discrete Fourier sum

Used byFFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · FFT after inverse FFT at the positive root is the identity · Inverse FFT after FFT at the positive root is the identity

DefinitionCharged entrywise conjugation#✓fully proved

For a type with a star operation \(z \mapsto \bar z\) and a vector \(x = (x_0, \dots, x_{n-1})\) of length \(n\) over it, this costed computation returns \((\bar x_0, \dots, \bar x_{n-1})\) and charges \(3n\) operations: one read, one conjugation and one write per entry.

def fftConjugate {R : Type u} [Star R] {n : Nat} (xs : Vector R n) :
    TimeM Nat (Vector R n) :=
  ⟨xs.map star, 3 * n⟩

Used by 5

Used byConjugating around the FFT conjugates the root · Inverse FFT by conjugation · The inverse FFT is a normalized FFT at the conjugate root · Exact operation count of the inverse FFT · Operation bound for the inverse FFT

DefinitionCharged entrywise scaling#✓fully proved

For a type with a multiplication, a scalar \(c\) and a vector \(x = (x_0, \dots, x_{n-1})\) of length \(n\) over it, this costed computation returns \((c x_0, \dots, c x_{n-1})\) and charges \(3n\) operations: one read, one multiplication and one write per entry.

def fftScale {R : Type u} [Mul R] {n : Nat} (scale : R) (xs : Vector R n) :
    TimeM Nat (Vector R n) :=
  ⟨xs.map (fun x => scale * x), 3 * n⟩

Used by 1

Used byInverse FFT by conjugation

DefinitionInverse FFT by conjugation#✓fully proved

Let \(R\) be a field that is a star ring, with star operation \(z \mapsto \bar z\). For a natural number \(d\), an element \(\omega \in R\) and a vector \(x \in R^{2^d}\), the inverse FFT conjugates every entry of \(x\), applies the radix-two FFT with root \(\omega\), conjugates every entry of the result, and multiplies every entry by the inverse \((2^d)^{-1}\) of \(2^d\) in \(R\) (which is \(0\) when \(2^d = 0\) in \(R\)). It charges \(3 \cdot 2^d\) operations for each of the two conjugation passes and for the scaling pass, one operation for computing \((2^d)^{-1}\), and the cost of the FFT.

def ifft {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    TimeM Nat (Vector R (2 ^ d)) := do
  let conjugated ← fftConjugate xs
  let transformed ← fft d omega conjugated
  let restored ← fftConjugate transformed
  let scale ← (⟨((2 ^ d : Nat) : R)⁻¹, 1⟩ : TimeM Nat R)
  fftScale scale restored

Uses 3 · Used by 15

Statement usesRadix-two fast Fourier transform · Charged entrywise conjugation · Charged entrywise scaling

Used byFFT circular convolution · Output of FFT circular convolution · FFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · Exact cost of FFT circular convolution · FFT after inverse FFT is the identity at the negative-sign root · FFT after inverse FFT at the positive root is the identity · Correctness of the inverse FFT · Inverse FFT after FFT is the identity at the negative-sign root · Inverse FFT after FFT at the positive root is the identity · The inverse FFT is a normalized FFT at the conjugate root · Inverse FFT at the negative-sign root computes the inverse DFT · Inverse FFT at the positive-sign root computes the normalized forward DFT · Exact operation count of the inverse FFT · Operation bound for the inverse FFT

DefinitionTimed pointwise product#✓fully proved

For a type \(R\) with a multiplication and vectors \(x, y\) of length \(n\) over \(R\), the pointwise product returns the vector of length \(n\) whose \(i\)-th entry is \(x_i \cdot y_i\) for every \(i < n\), and charges \(4n\) time units: two reads, one multiplication and one write per entry.

def fftPointwise {R : Type u} [Mul R] {n : Nat} (xs ys : Vector R n) :
    TimeM Nat (Vector R n) :=
  ⟨xs.zipWith (fun x y => x * y) ys, 4 * n⟩

Used by 6

Used byFFT circular convolution · Output of FFT circular convolution · FFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · Exact cost of FFT circular convolution · Entries of the pointwise product

DefinitionZero padding to twice the length#✓fully proved

For a type \(R\) with a zero, a natural number \(d\) and a vector \(x\) of length \(2^d\) over \(R\), padding returns the vector of length \(2^{d+1}\) whose \(i\)-th entry is \(x_i\) for \(i < 2^d\) and \(0\) for \(2^d \le i < 2^{d+1}\), and charges \(3 \cdot 2^d\) time units.

def fftPad {R : Type u} [Zero R] (d : Nat) (xs : Vector R (2 ^ d)) :
    TimeM Nat (Vector R (2 ^ (d + 1))) :=
  ⟨Vector.ofFn (fun i => if h : i.val < 2 ^ d then xs[i.val] else 0), 3 * 2 ^ d⟩

Used by 9

Used byFFT linear convolution · Output of FFT linear convolution · FFT linear convolution gives the product coefficients (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign) · Exact cost of FFT linear convolution · Zero padding turns cyclic convolution into the polynomial product · Zero padding fills the second half with zeros · Zero padding keeps the input prefix · Zero padding preserves the polynomial

DefinitionFFT circular convolution#✓fully proved

Let \(R\) be a field that is a star ring, \(d\) a natural number, \(\omega \in R\), and \(x, y\) vectors of length \(2^d\) over \(R\). Circular convolution runs the timed radix-two FFT of length \(2^d\) with root \(\omega\) on \(x\) and then on \(y\), multiplies the two transforms pointwise, and applies the timed inverse FFT of length \(2^d\) with root \(\omega\) to the product. It returns the result of the inverse transform, and its cost is the sum of the costs of these four steps.

The definition imposes no condition on \(\omega\).

def fftCircular {R : Type u} [Field R] [StarRing R] (d : Nat)
    (omega : R) (xs ys : Vector R (2 ^ d)) : TimeM Nat (Vector R (2 ^ d)) := do
  let left ← fft d omega xs
  let right ← fft d omega ys
  let product ← fftPointwise left right
  ifft d omega product

Uses 3 · Used by 16

Statement usesRadix-two fast Fourier transform · Timed pointwise product · Inverse FFT by conjugation

Used byFFT circular convolution on arrays · Rejection by array circular convolution · Array circular FFT convolution agrees with the vector version · Output length of array circular FFT convolution · Exact cost of array circular FFT convolution · Array circular FFT convolution costs the same as the vector version · Output of FFT circular convolution · FFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · Exact cost of FFT circular convolution · Cost bound for FFT circular convolution · FFT linear convolution · Output of FFT linear convolution · FFT linear convolution gives the product coefficients (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign) · Exact cost of FFT linear convolution

DefinitionFFT linear convolution#✓fully proved

Let \(R\) be a field that is a star ring, \(d\) a natural number, \(\omega \in R\), and \(x, y\) vectors of length \(2^d\) over \(R\). Linear convolution zero-pads \(x\) and \(y\) to length \(2^{d+1}\) and returns the FFT circular convolution of the two padded vectors at length \(2^{d+1}\) with root \(\omega\). Its cost is the cost of the two paddings plus the cost of the circular convolution.

The root \(\omega\) is used for the padded length \(2^{d+1}\), twice the input length.

def fftLinear {R : Type u} [Field R] [StarRing R] (d : Nat)
    (omega : R) (xs ys : Vector R (2 ^ d)) :
    TimeM Nat (Vector R (2 ^ (d + 1))) := do
  let left ← fftPad d xs
  let right ← fftPad d ys
  fftCircular (d + 1) omega left right

Uses 2 · Used by 17

Statement usesFFT circular convolution · Zero padding to twice the length

Used byFFT linear convolution on arrays · Rejection by array linear convolution · Array linear FFT convolution agrees with the vector version · Output length of array linear FFT convolution · Exact cost of array linear FFT convolution · Array linear FFT convolution costs the same as the vector version · Output of FFT linear convolution · FFT linear convolution gives the product coefficients (Princeton sign) · The last entry of FFT linear convolution is zero (Princeton sign) · FFT linear convolution computes the convolution sums (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign) · The last entry of FFT linear convolution is zero (MIT/CLRS sign) · FFT linear convolution computes the convolution sums (MIT/CLRS sign) · Exact cost of FFT linear convolution · Cost bound for FFT linear convolution · FFT linear convolution returns the product polynomial (Princeton sign) · FFT linear convolution returns the product polynomial (MIT/CLRS sign)

DefinitionFFT circular convolution on arrays#✓fully proved

Let \(R\) be a field that is a star ring, \(\omega \in R\), and \(x, y\) arrays over \(R\), where \(x\) has length \(n\). If \(n = 2^d\) for some natural number \(d\) and \(y\) also has length \(n\), the procedure returns the FFT circular convolution of \(x\) and \(y\) (read as vectors of length \(2^d\)) with root \(\omega\), converted to an array, at the cost of that convolution. Otherwise it returns no result, at cost \(0\).

def fftCircularArray {R : Type u} [Field R] [StarRing R] (omega : R)
    (xs ys : Array R) : TimeM Nat (Option (Array R)) :=
  if h : xs.size = 2 ^ xs.size.log2 ∧ ys.size = xs.size then
    let left : Vector R (2 ^ xs.size.log2) := ⟨xs, h.1⟩
    let right : Vector R (2 ^ xs.size.log2) := ⟨ys, h.2.trans h.1⟩
    do
      let out ← fftCircular xs.size.log2 omega left right
      pure (some out.toArray)
  else pure none

Uses 1 · Used by 5

Statement usesFFT circular convolution

Used byRejection by array circular convolution · Array circular FFT convolution agrees with the vector version · Output length of array circular FFT convolution · Exact cost of array circular FFT convolution · Array circular FFT convolution costs the same as the vector version

DefinitionFFT linear convolution on arrays#✓fully proved

Let \(R\) be a field that is a star ring, \(\omega \in R\), and \(x, y\) arrays over \(R\), where \(x\) has length \(n\). If \(n = 2^d\) for some natural number \(d\) and \(y\) also has length \(n\), the procedure returns the FFT linear convolution of \(x\) and \(y\) (read as vectors of length \(2^d\)) with root \(\omega\), an array of length \(2n\), at the cost of that convolution. Otherwise it returns no result, at cost \(0\).

def fftLinearArray {R : Type u} [Field R] [StarRing R] (omega : R)
    (xs ys : Array R) : TimeM Nat (Option (Array R)) :=
  if h : xs.size = 2 ^ xs.size.log2 ∧ ys.size = xs.size then
    let left : Vector R (2 ^ xs.size.log2) := ⟨xs, h.1⟩
    let right : Vector R (2 ^ xs.size.log2) := ⟨ys, h.2.trans h.1⟩
    do
      let out ← fftLinear xs.size.log2 omega left right
      pure (some out.toArray)
  else pure none

Uses 1 · Used by 5

Statement usesFFT linear convolution

Used byRejection by array linear convolution · Array linear FFT convolution agrees with the vector version · Output length of array linear FFT convolution · Exact cost of array linear FFT convolution · Array linear FFT convolution costs the same as the vector version

TheoremEntries of the pointwise product#✓fully proved

Let \(R\) be a type with a multiplication, let \(n\) be a natural number and let \(x\) and \(y\) be vectors of length \(n\) over \(R\). For every index \(i < n\), entry \(i\) of the pointwise product of \(x\) and \(y\) equals \(x_i y_i\).

theorem fftPointwise_ret {R : Type u} [Mul R] {n : Nat}
    (xs ys : Vector R n) (i : Fin n) :
    (fftPointwise xs ys).ret[i.val] = xs[i.val] * ys[i.val]

Uses 1 · Used by 2

Statement usesTimed pointwise product

Used byFFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution

TheoremZero padding keeps the input prefix#✓fully proved

Let \(R\) be a type with a zero, let \(d\) be a natural number and let \(x\) be a vector of length \(2^d\) over \(R\). For every index \(i < 2^d\), entry \(i\) of the zero-padded vector of length \(2^{d+1}\) produced from \(x\) equals \(x_i\).

theorem fftPad_ret_low {R : Type u} [Zero R] (d : Nat)
    (xs : Vector R (2 ^ d)) (i : Fin (2 ^ d)) :
    (fftPad d xs).ret[i.val]'(by
      have h := i.isLt
      simp only [pow_succ]
      omega) = xs[i.val]

Uses 1 · Used by 1

Statement usesZero padding to twice the length

Used byZero padding preserves the polynomial

TheoremZero padding fills the second half with zeros#✓fully proved

Let \(R\) be a type with a zero, let \(d\) be a natural number and let \(x\) be a vector of length \(2^d\) over \(R\). For every index \(i\) with \(2^d \le i < 2^{d+1}\), entry \(i\) of the zero-padded vector of length \(2^{d+1}\) produced from \(x\) is \(0\).

theorem fftPad_ret_high {R : Type u} [Zero R] (d : Nat)
    (xs : Vector R (2 ^ d)) (i : Fin (2 ^ (d + 1))) (hi : 2 ^ d ≤ i.val) :
    (fftPad d xs).ret[i.val] = 0

Uses 1 · Used by 1

Statement usesZero padding to twice the length

Used byZero padding preserves the polynomial

TheoremRejection by array circular convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(\omega \in R\), and let \(x\) and \(y\) be arrays over \(R\). The array circular-convolution procedure with root \(\omega\) returns no result on \(x\) and \(y\) if and only if it is not the case that the length of \(x\) is a power of two \(2^k\) with \(k \ge 0\) and \(y\) has the same length as \(x\).

theorem fftCircularArray_eq_none_iff {R : Type u} [Field R] [StarRing R]
    (omega : R) (xs ys : Array R) :
    (fftCircularArray omega xs ys).ret = none ↔
      ¬ (xs.size = 2 ^ xs.size.log2 ∧ ys.size = xs.size)

Uses 2

Statement usesFFT circular convolution on arrays

Proof usesFFT circular convolution

TheoremRejection by array linear convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(\omega \in R\), and let \(x\) and \(y\) be arrays over \(R\). The array zero-padded linear-convolution procedure with root \(\omega\) returns no result on \(x\) and \(y\) if and only if it is not the case that the length of \(x\) is a power of two \(2^k\) with \(k \ge 0\) and \(y\) has the same length as \(x\).

theorem fftLinearArray_eq_none_iff {R : Type u} [Field R] [StarRing R]
    (omega : R) (xs ys : Array R) :
    (fftLinearArray omega xs ys).ret = none ↔
      ¬ (xs.size = 2 ^ xs.size.log2 ∧ ys.size = xs.size)

Uses 2

Statement usesFFT linear convolution on arrays

Proof usesFFT linear convolution

TheoremConjugating around the FFT conjugates the root#✓fully proved

Let \(N = 2^d\), let \(\omega \in \mathbb{C}\) be a primitive \(N\)-th root of unity and let \(x \in \mathbb{C}^N\). Conjugating every entry of \(x\), running the FFT procedure with root \(\omega\) and conjugating every entry of the result gives the same vector as running the FFT procedure on \(x\) with root \(\overline{\omega}\).

theorem fft_conjugate_ret (d : Nat) (omega : ℂ)
    (hroot : IsPrimitiveRoot omega (2 ^ d)) (xs : Vector ℂ (2 ^ d)) :
    (fftConjugate (fft d omega (fftConjugate xs).ret).ret).ret =
      (fft d (star omega) xs).ret

Uses 4 · Used by 1

Statement usesRadix-two fast Fourier transform · Charged entrywise conjugation

Proof usesCorrectness of the radix-two FFT · Discrete Fourier sum

Used byThe inverse FFT is a normalized FFT at the conjugate root

TheoremThe inverse FFT is a normalized FFT at the conjugate root#✓fully proved

Let \(N = 2^d\), let \(\omega \in \mathbb{C}\) be a primitive \(N\)-th root of unity and let \(x \in \mathbb{C}^N\). The output of the inverse FFT procedure on \(x\) with root \(\omega\) is the output of the FFT procedure on \(x\) with root \(\overline{\omega}\) with every entry multiplied by \(N^{-1}\).

theorem ifft_ret (d : Nat) (omega : ℂ)
    (hroot : IsPrimitiveRoot omega (2 ^ d)) (xs : Vector ℂ (2 ^ d)) :
    (ifft d omega xs).ret =
      (fft d (star omega) xs).ret.map (fun x => (2 ^ d : ℂ)⁻¹ * x)

Uses 4 · Used by 1

Statement usesRadix-two fast Fourier transform · Inverse FFT by conjugation

Proof usesCharged entrywise conjugation · Conjugating around the FFT conjugates the root

Used byCorrectness of the inverse FFT

TheoremCorrectness of the inverse FFT#✓fully proved

Let \(N = 2^d\), let \(\omega \in \mathbb{C}\) be a primitive \(N\)-th root of unity and let \(x \in \mathbb{C}^N\). For every \(k < N\), entry \(k\) of the output of the inverse FFT procedure on \(x\) with root \(\omega\) equals \(N^{-1}\) times the discrete Fourier sum of length \(N\) with root \(\overline{\omega}\) at frequency \(k\) of the sequence \(j \mapsto x_j\) (set to \(0\) for \(j \ge N\)), that is, \(N^{-1} \sum_{j=0}^{N-1} \overline{\omega}^{jk} x_j\).

theorem ifft_correct (d : Nat) (omega : ℂ)
    (hroot : IsPrimitiveRoot omega (2 ^ d)) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (ifft d omega xs).ret[k.val] =
      (2 ^ d : ℂ)⁻¹ *
        dftSum (2 ^ d) (star omega) (fun j => xs.toArray.getD j 0) k.val

Uses 5 · Used by 2

Statement usesInverse FFT by conjugation · Discrete Fourier sum

Proof usesRadix-two fast Fourier transform · Correctness of the radix-two FFT · The inverse FFT is a normalized FFT at the conjugate root

Used byInverse FFT at the negative-sign root computes the inverse DFT · Inverse FFT at the positive-sign root computes the normalized forward DFT

TheoremInverse FFT at the negative-sign root computes the inverse DFT#✓fully proved

Let \(N = 2^d\) and \(x \in \mathbb{C}^N\), and run the inverse FFT procedure on \(x\) with root \(e^{-2\pi i/N}\), the value at \(-1\) of the standard additive character of \(\mathbb{Z}/N\mathbb{Z}\). For every \(k < N\), entry \(k\) of its output equals the canonical inverse discrete Fourier transform of the function on \(\mathbb{Z}/N\mathbb{Z}\) sending the class of \(j < N\) to \(x_j\), evaluated at the class of \(k\); that is, it equals \(N^{-1} \sum_{j=0}^{N-1} e^{2\pi i jk/N} x_j\).

theorem ifft_stdAddChar_neg_one (d : Nat) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (ifft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d))) xs).ret[k.val] =
      ZMod.dft.symm (fun j : ZMod (2 ^ d) => xs.toArray.getD j.val 0)
        (k.val : ZMod (2 ^ d))

Uses 3 · Used by 3

Statement usesInverse FFT by conjugation

Proof usesCorrectness of the inverse FFT · Discrete Fourier sum

Used byFFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT after inverse FFT is the identity at the negative-sign root · Inverse FFT after FFT is the identity at the negative-sign root

TheoremInverse FFT at the positive-sign root computes the normalized forward DFT#✓fully proved

Let \(N = 2^d\) and \(x \in \mathbb{C}^N\), and run the inverse FFT procedure on \(x\) with root \(e^{2\pi i/N}\), the value at \(1\) of the standard additive character of \(\mathbb{Z}/N\mathbb{Z}\). For every \(k < N\), entry \(k\) of its output equals \(N^{-1}\) times the canonical discrete Fourier transform of the function on \(\mathbb{Z}/N\mathbb{Z}\) sending the class of \(j < N\) to \(x_j\), evaluated at the class of \(k\); that is, it equals \(N^{-1} \sum_{j=0}^{N-1} e^{-2\pi i jk/N} x_j\).

theorem ifft_stdAddChar_one (d : Nat) (xs : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (ifft d (ZMod.stdAddChar (1 : ZMod (2 ^ d))) xs).ret[k.val] =
      (2 ^ d : ℂ)⁻¹ * ZMod.dft (fun j : ZMod (2 ^ d) => xs.toArray.getD j.val 0)
        (k.val : ZMod (2 ^ d))

Uses 3 · Used by 3

Statement usesInverse FFT by conjugation

Proof usesCorrectness of the inverse FFT · Discrete Fourier sum

Used byFFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · FFT after inverse FFT at the positive root is the identity · Inverse FFT after FFT at the positive root is the identity

TheoremInverse FFT after FFT is the identity at the negative-sign root#✓fully proved

Let \(N = 2^d\) and let \(\omega = e^{-2\pi i/N}\), the value at \(-1\) of the standard additive character of \(\mathbb{Z}/N\mathbb{Z}\). For every \(x \in \mathbb{C}^N\), running the FFT procedure on \(x\) with root \(\omega\) and then the inverse FFT procedure on its output with root \(\omega\) returns \(x\).

theorem ifft_fft_stdAddChar_neg_one (d : Nat) (xs : Vector ℂ (2 ^ d)) :
    (ifft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d)))
      (fft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d))) xs).ret).ret = xs

Uses 4

Statement usesRadix-two fast Fourier transform · Inverse FFT by conjugation

Proof usesThe radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · Inverse FFT at the negative-sign root computes the inverse DFT

TheoremFFT after inverse FFT is the identity at the negative-sign root#✓fully proved

Let \(N = 2^d\) and let \(\omega = e^{-2\pi i/N}\), the value at \(-1\) of the standard additive character of \(\mathbb{Z}/N\mathbb{Z}\). For every \(x \in \mathbb{C}^N\), running the inverse FFT procedure on \(x\) with root \(\omega\) and then the FFT procedure on its output with root \(\omega\) returns \(x\).

theorem fft_ifft_stdAddChar_neg_one (d : Nat) (xs : Vector ℂ (2 ^ d)) :
    (fft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d)))
      (ifft d (ZMod.stdAddChar (-1 : ZMod (2 ^ d))) xs).ret).ret = xs

Uses 4

Statement usesRadix-two fast Fourier transform · Inverse FFT by conjugation

Proof usesThe radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · Inverse FFT at the negative-sign root computes the inverse DFT

TheoremOutput of FFT circular convolution#✓fully proved

Let \(R\) be a field with a star-ring conjugation, let \(n = 2^d\), \(\omega \in R\) and \(x, y \in R^n\). The vector returned by FFT circular convolution of \(x\) and \(y\) with root \(\omega\) equals the vector returned by the inverse FFT with root \(\omega\) applied to the vector returned by pointwise multiplication of \(\hat{x}\) and \(\hat{y}\), where \(\hat{x}\) and \(\hat{y}\) are the vectors returned by the radix-two FFT of \(x\) and of \(y\) with root \(\omega\).

Only returned values are compared; operation counts are not.

theorem fftCircular_ret {R : Type u} [Field R] [StarRing R] (d : Nat)
    (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircular d omega xs ys).ret =
      (ifft d omega (fftPointwise (fft d omega xs).ret (fft d omega ys).ret).ret).ret

Uses 4 · Used by 2

Statement usesRadix-two fast Fourier transform · FFT circular convolution · Timed pointwise product · Inverse FFT by conjugation

Used byFFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution

TheoremOutput of FFT linear convolution#✓fully proved

Let \(R\) be a field with a star-ring conjugation, let \(\omega \in R\) and \(x, y \in R^{2^d}\). The vector returned by FFT linear convolution of \(x\) and \(y\) with root \(\omega\) equals the vector returned by FFT circular convolution, at length \(2^{d+1}\) with root \(\omega\), of the vectors returned by zero-padding \(x\) and \(y\) to length \(2^{d+1}\).

Only returned values are compared; operation counts are not.

theorem fftLinear_ret {R : Type u} [Field R] [StarRing R] (d : Nat)
    (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinear d omega xs ys).ret =
      (fftCircular (d + 1) omega (fftPad d xs).ret (fftPad d ys).ret).ret

Uses 3 · Used by 2

Statement usesFFT circular convolution · FFT linear convolution · Zero padding to twice the length

Used byFFT linear convolution gives the product coefficients (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign)

TheoremFFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution#✓fully proved

Let \(n = 2^d\) and \(x, y \in \mathbb{C}^n\). Run FFT circular convolution of \(x\) and \(y\) with root \(\omega = e^{-2\pi i/n}\), the value at \(-1\) of the standard additive character of \(\mathbb{Z}/n\mathbb{Z}\). Then for every \(k < n\), entry \(k\) of the returned vector equals \(\sum_{j \in \mathbb{Z}/n\mathbb{Z}} x_j \, y_{k - j}\), with indices taken modulo \(n\).

This root is the sign convention of the Princeton (Sedgewick–Wayne) source.

theorem fftCircular_stdAddChar_neg_one (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (fftCircular d (ZMod.stdAddChar (-1 : ZMod (2 ^ d))) xs ys).ret[k.val] =
      ∑ j : ZMod (2 ^ d), xs.toArray.getD j.val 0 *
        ys.toArray.getD ((k.val : ZMod (2 ^ d)) - j).val 0

Uses 9 · Used by 1

Statement usesFFT circular convolution

Proof usesRadix-two fast Fourier transform · Output of FFT circular convolution · Timed pointwise product · Entries of the pointwise product · The radix-two FFT with root \(e^{-2\pi i/n}\) computes the DFT · Inverse FFT by conjugation · Inverse FFT at the negative-sign root computes the inverse DFT · Convolution theorem for the discrete Fourier transform

Used byFFT linear convolution gives the product coefficients (Princeton sign)

TheoremFFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution#✓fully proved

Let \(n = 2^d\) and \(x, y \in \mathbb{C}^n\). Run FFT circular convolution of \(x\) and \(y\) with root \(\omega = e^{2\pi i/n}\), the value at \(1\) of the standard additive character of \(\mathbb{Z}/n\mathbb{Z}\). Then for every \(k < n\), entry \(k\) of the returned vector equals \(\sum_{j \in \mathbb{Z}/n\mathbb{Z}} x_j \, y_{k - j}\), with indices taken modulo \(n\).

This root is the sign convention of the MIT and CLRS sources.

theorem fftCircular_stdAddChar_one (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ d)) :
    (fftCircular d (ZMod.stdAddChar (1 : ZMod (2 ^ d))) xs ys).ret[k.val] =
      ∑ j : ZMod (2 ^ d), xs.toArray.getD j.val 0 *
        ys.toArray.getD ((k.val : ZMod (2 ^ d)) - j).val 0

Uses 9 · Used by 1

Statement usesFFT circular convolution

Proof usesRadix-two fast Fourier transform · Output of FFT circular convolution · Timed pointwise product · Entries of the pointwise product · The radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Inverse FFT by conjugation · Inverse FFT at the positive-sign root computes the normalized forward DFT · Convolution theorem for the discrete Fourier transform

Used byFFT linear convolution gives the product coefficients (MIT/CLRS sign)

TheoremExact operation count of the inverse FFT#✓fully proved

Let \(R\) be a field with a star ring structure, let \(d\) be a natural number, \(N = 2^d\), \(\omega \in R\) arbitrary and \(x \in R^N\). The number \(T\) of operations charged by the inverse FFT procedure on \(x\) with root \(\omega\) satisfies \(T + 1 = (7d + 10) \cdot 2^d + 1\), equivalently \(T = (7d + 10) \cdot 2^d\).

Beyond the FFT, the two conjugation passes and the scaling pass each charge \(3N\) operations and computing \(1/N\) charges one, for \(9N + 1\) in total.

theorem ifft_time_add_one {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (ifft d omega xs).time + 1 = (7 * d + 10) * 2 ^ d + 1

Uses 4 · Used by 1

Statement usesInverse FFT by conjugation

Proof usesRadix-two fast Fourier transform · Charged entrywise conjugation · Exact cost of the radix-two FFT

Used byExact cost of FFT circular convolution

TheoremOperation bound for the inverse FFT#✓fully proved

Let \(R\) be a field with a star ring structure, let \(d\) be a natural number, \(N = 2^d\), \(\omega \in R\) arbitrary and \(x \in R^N\). The number of operations charged by the inverse FFT procedure on \(x\) with root \(\omega\) is at most \(8 \cdot 2^d \cdot d + 9 \cdot 2^d + 1\).

theorem ifft_time_le {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs : Vector R (2 ^ d)) :
    (ifft d omega xs).time ≤ 8 * (2 ^ d) * d + 9 * (2 ^ d) + 1

Uses 4

Statement usesInverse FFT by conjugation

Proof usesRadix-two fast Fourier transform · Charged entrywise conjugation · Cost bound for the radix-two FFT

TheoremExact cost of FFT circular convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x\) and \(y\) be vectors of length \(2^d\) over \(R\). The cost charged by circular convolution of \(x\) and \(y\) with root \(\omega\), plus \(2\), equals \((21d + 16) \cdot 2^d\).

The cost is the sum of the costs of the two forward transforms, the pointwise product and the inverse transform.

theorem fftCircular_time_add_two {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircular d omega xs ys).time + 2 = (21 * d + 16) * 2 ^ d

Uses 6 · Used by 3

Statement usesFFT circular convolution

Proof usesRadix-two fast Fourier transform · Timed pointwise product · Exact cost of the radix-two FFT · Inverse FFT by conjugation · Exact operation count of the inverse FFT

Used byExact cost of array circular FFT convolution · Cost bound for FFT circular convolution · Exact cost of FFT linear convolution

TheoremCost bound for FFT circular convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x\) and \(y\) be vectors of length \(2^d\) over \(R\). The cost charged by circular convolution of \(x\) and \(y\) with root \(\omega\) is at most \((21d + 16) \cdot 2^d\), that is, \(21 n \log_2 n + 16 n\) for the input length \(n = 2^d\).

theorem fftCircular_time_le {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircular d omega xs ys).time ≤ (21 * d + 16) * 2 ^ d

Uses 2

Statement usesFFT circular convolution

Proof usesExact cost of FFT circular convolution

TheoremExact cost of FFT linear convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x\) and \(y\) be vectors of length \(2^d\) over \(R\). The cost charged by zero-padded linear convolution of \(x\) and \(y\) with root \(\omega\), plus \(2\), equals \((42d + 80) \cdot 2^d\).

The cost is that of zero padding both inputs to length \(2^{d+1}\) plus that of circular convolution at length \(2^{d+1}\).

theorem fftLinear_time_add_two {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinear d omega xs ys).time + 2 = (42 * d + 80) * 2 ^ d

Uses 4 · Used by 2

Statement usesFFT linear convolution

Proof usesFFT circular convolution · Exact cost of FFT circular convolution · Zero padding to twice the length

Used byExact cost of array linear FFT convolution · Cost bound for FFT linear convolution

TheoremCost bound for FFT linear convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x\) and \(y\) be vectors of length \(2^d\) over \(R\). The cost charged by zero-padded linear convolution of \(x\) and \(y\) with root \(\omega\) is at most \((42d + 80) \cdot 2^d\), that is, \(42 n \log_2 n + 80 n\) for the input length \(n = 2^d\).

theorem fftLinear_time_le {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinear d omega xs ys).time ≤ (42 * d + 80) * 2 ^ d

Uses 2

Statement usesFFT linear convolution

Proof usesExact cost of FFT linear convolution

TheoremArray circular FFT convolution agrees with the vector version#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\) be arbitrary, and let \(x, y\) be vectors over \(R\) of length \(2^d\). Then array circular FFT convolution with root \(\omega\), run on the arrays underlying \(x\) and \(y\), succeeds and returns the array underlying the output of vector circular FFT convolution of \(x\) and \(y\) at size \(2^d\) with root \(\omega\).

theorem fftCircularArray_ret_of_vector {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircularArray omega xs.toArray ys.toArray).ret =
      some (fftCircular d omega xs ys).ret.toArray

Uses 2

Statement usesFFT circular convolution · FFT circular convolution on arrays

TheoremArray circular FFT convolution costs the same as the vector version#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x, y\) be vectors over \(R\) of length \(2^d\). The time charged by array circular FFT convolution with root \(\omega\) on the arrays underlying \(x\) and \(y\) equals the time charged by vector circular FFT convolution of \(x\) and \(y\) at size \(2^d\) with root \(\omega\).

theorem fftCircularArray_time_of_vector {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircularArray omega xs.toArray ys.toArray).time = (fftCircular d omega xs ys).time

Uses 2 · Used by 1

Statement usesFFT circular convolution · FFT circular convolution on arrays

Used byExact cost of array circular FFT convolution

TheoremExact cost of array circular FFT convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x, y\) be vectors over \(R\) of length \(2^d\). The time charged by array circular FFT convolution with root \(\omega\) on the arrays underlying \(x\) and \(y\), plus \(2\), equals \((21d + 16) \cdot 2^d\).

theorem fftCircularArray_time_add_two {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftCircularArray omega xs.toArray ys.toArray).time + 2 = (21 * d + 16) * 2 ^ d

Uses 4

Statement usesFFT circular convolution on arrays

Proof usesFFT circular convolution · Array circular FFT convolution costs the same as the vector version · Exact cost of FFT circular convolution

TheoremOutput length of array circular FFT convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(\omega \in R\), and let \(x, y\) be arrays over \(R\). If array circular FFT convolution with root \(\omega\) on \(x\) and \(y\) returns an array \(z\), then \(z\) has the same length as \(x\).

theorem fftCircularArray_size_of_eq_some {R : Type u} [Field R] [StarRing R]
    (omega : R) (xs ys out : Array R)
    (hout : (fftCircularArray omega xs ys).ret = some out) :
    out.size = xs.size

Uses 2

Statement usesFFT circular convolution on arrays

Proof usesFFT circular convolution

TheoremArray linear FFT convolution agrees with the vector version#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\) be arbitrary, and let \(x, y\) be vectors over \(R\) of length \(2^d\). Then array zero-padded linear FFT convolution with root \(\omega\), run on the arrays underlying \(x\) and \(y\), succeeds and returns the array underlying the output (of length \(2^{d+1}\)) of vector zero-padded linear FFT convolution of \(x\) and \(y\) at size \(2^d\) with root \(\omega\).

theorem fftLinearArray_ret_of_vector {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinearArray omega xs.toArray ys.toArray).ret =
      some (fftLinear d omega xs ys).ret.toArray

Uses 2

Statement usesFFT linear convolution · FFT linear convolution on arrays

TheoremArray linear FFT convolution costs the same as the vector version#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x, y\) be vectors over \(R\) of length \(2^d\). The time charged by array zero-padded linear FFT convolution with root \(\omega\) on the arrays underlying \(x\) and \(y\) equals the time charged by vector zero-padded linear FFT convolution of \(x\) and \(y\) at size \(2^d\) with root \(\omega\).

theorem fftLinearArray_time_of_vector {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinearArray omega xs.toArray ys.toArray).time = (fftLinear d omega xs ys).time

Uses 2 · Used by 1

Statement usesFFT linear convolution · FFT linear convolution on arrays

Used byExact cost of array linear FFT convolution

TheoremExact cost of array linear FFT convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(d\) be a natural number, let \(\omega \in R\), and let \(x, y\) be vectors over \(R\) of length \(2^d\). The time charged by array zero-padded linear FFT convolution with root \(\omega\) on the arrays underlying \(x\) and \(y\), plus \(2\), equals \((42d + 80) \cdot 2^d\).

theorem fftLinearArray_time_add_two {R : Type u} [Field R] [StarRing R]
    (d : Nat) (omega : R) (xs ys : Vector R (2 ^ d)) :
    (fftLinearArray omega xs.toArray ys.toArray).time + 2 = (42 * d + 80) * 2 ^ d

Uses 4

Statement usesFFT linear convolution on arrays

Proof usesFFT linear convolution · Array linear FFT convolution costs the same as the vector version · Exact cost of FFT linear convolution

TheoremOutput length of array linear FFT convolution#✓fully proved

Let \(R\) be a field with a star-ring structure, let \(\omega \in R\), and let \(x, y\) be arrays over \(R\). If array zero-padded linear FFT convolution with root \(\omega\) on \(x\) and \(y\) returns an array \(z\), then the length of \(z\) is twice the length of \(x\).

theorem fftLinearArray_size_of_eq_some {R : Type u} [Field R] [StarRing R]
    (omega : R) (xs ys out : Array R)
    (hout : (fftLinearArray omega xs ys).ret = some out) :
    out.size = 2 * xs.size

Uses 2

Statement usesFFT linear convolution on arrays

Proof usesFFT linear convolution

DefinitionPolynomial of a coefficient vector#✓fully proved

The polynomial of a vector \(x = (x_0, \dots, x_{n-1}) \in \mathbb{C}^n\) is \(\sum_{j=0}^{n-1} x_j X^j \in \mathbb{C}[X]\), the complex polynomial whose coefficient of \(X^j\) is \(x_j\) for \(j < n\) and \(0\) for \(j \ge n\).

noncomputable def fftPolynomial {n : Nat} (xs : Vector ℂ n) : Polynomial ℂ := by
  classical
  exact Polynomial.ofFn n (fun j : Fin n => xs[j.val])

Used by 14

Used byFFT linear convolution gives the product coefficients (Princeton sign) · The last entry of FFT linear convolution is zero (Princeton sign) · FFT linear convolution computes the convolution sums (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign) · The last entry of FFT linear convolution is zero (MIT/CLRS sign) · FFT linear convolution computes the convolution sums (MIT/CLRS sign) · Zero padding turns cyclic convolution into the polynomial product · Coefficients of the polynomial of a vector · FFT linear convolution returns the product polynomial (Princeton sign) · FFT linear convolution returns the product polynomial (MIT/CLRS sign) · Zero padding preserves the polynomial · Coefficients of a product of vector polynomials · Coefficients of a product beyond twice the length vanish · The last coefficient of a doubled-length product vanishes

TheoremCoefficients of the polynomial of a vector#✓fully proved

For every vector \(x = (x_0, \dots, x_{n-1}) \in \mathbb{C}^n\) and every natural number \(k\), the coefficient of \(X^k\) in the polynomial of \(x\) is \(x_k\) if \(k < n\) and \(0\) if \(k \ge n\).

theorem fftPolynomial_coeff {n : Nat} (xs : Vector ℂ n) (k : Nat) :
    (fftPolynomial xs).coeff k = xs.toArray.getD k 0

Uses 1 · Used by 5

Statement usesPolynomial of a coefficient vector

Used byZero padding turns cyclic convolution into the polynomial product · FFT linear convolution returns the product polynomial (Princeton sign) · FFT linear convolution returns the product polynomial (MIT/CLRS sign) · Zero padding preserves the polynomial · Coefficients of a product of vector polynomials

TheoremZero padding preserves the polynomial#✓fully proved

For every natural number \(d\) and every vector \(x \in \mathbb{C}^{2^d}\), the zero padding of \(x\) (the vector of length \(2^{d+1}\) whose first \(2^d\) entries are those of \(x\) and whose remaining entries are \(0\)) has the same polynomial as \(x\).

theorem fftPolynomial_fftPad (d : Nat) (xs : Vector ℂ (2 ^ d)) :
    fftPolynomial (fftPad d xs).ret = fftPolynomial xs

Uses 5 · Used by 1

Statement usesZero padding to twice the length · Polynomial of a coefficient vector

Proof usesZero padding fills the second half with zeros · Zero padding keeps the input prefix · Coefficients of the polynomial of a vector

Used byZero padding turns cyclic convolution into the polynomial product

TheoremCoefficients of a product of vector polynomials#✓fully proved

Let \(x, y \in \mathbb{C}^n\), and set \(x_i = y_i = 0\) for \(i \ge n\). For every natural number \(k\), the coefficient of \(X^k\) in the product of the polynomials of \(x\) and \(y\) is \(\sum_{j=0}^{k} x_j y_{k-j}\).

theorem fftPolynomial_mul_coeff {n : Nat} (xs ys : Vector ℂ n) (k : Nat) :
    (fftPolynomial xs * fftPolynomial ys).coeff k =
      ∑ j ∈ Finset.range (k + 1), xs.toArray.getD j 0 * ys.toArray.getD (k - j) 0

Uses 2 · Used by 5

Statement usesPolynomial of a coefficient vector

Proof usesCoefficients of the polynomial of a vector

Used byFFT linear convolution computes the convolution sums (Princeton sign) · FFT linear convolution computes the convolution sums (MIT/CLRS sign) · Zero padding turns cyclic convolution into the polynomial product · Coefficients of a product beyond twice the length vanish · The last coefficient of a doubled-length product vanishes

TheoremThe last coefficient of a doubled-length product vanishes#✓fully proved

For every natural number \(d\) and all vectors \(x, y \in \mathbb{C}^{2^d}\), the coefficient of \(X^{2 \cdot 2^d - 1}\) in the product of the polynomials of \(x\) and \(y\) is \(0\).

theorem fftPolynomial_mul_last (d : Nat) (xs ys : Vector ℂ (2 ^ d)) :
    (fftPolynomial xs * fftPolynomial ys).coeff (2 * 2 ^ d - 1) = 0

Uses 2 · Used by 2

Statement usesPolynomial of a coefficient vector

Proof usesCoefficients of a product of vector polynomials

Used byThe last entry of FFT linear convolution is zero (Princeton sign) · The last entry of FFT linear convolution is zero (MIT/CLRS sign)

TheoremCoefficients of a product beyond twice the length vanish#✓fully proved

For all vectors \(x, y \in \mathbb{C}^n\) and every natural number \(k \ge 2n\), the coefficient of \(X^k\) in the product of the polynomials of \(x\) and \(y\) is \(0\).

theorem fftPolynomial_mul_coeff_eq_zero_of_two_mul_le {n : Nat}
    (xs ys : Vector ℂ n) (k : Nat) (hk : 2 * n ≤ k) :
    (fftPolynomial xs * fftPolynomial ys).coeff k = 0

Uses 2 · Used by 2

Statement usesPolynomial of a coefficient vector

Proof usesCoefficients of a product of vector polynomials

Used byFFT linear convolution returns the product polynomial (Princeton sign) · FFT linear convolution returns the product polynomial (MIT/CLRS sign)

TheoremZero padding turns cyclic convolution into the polynomial product#✓fully proved

Let \(d\) be a natural number and \(N = 2^{d+1}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), write \(P_x = \sum_{j < 2^d} x_j X^j\) and \(P_y = \sum_{j < 2^d} y_j X^j\), and let \(x', y' \in \mathbb{C}^N\) be their zero paddings to length \(N\) (\(x'_j = x_j\) for \(j < 2^d\) and \(x'_j = 0\) otherwise, and likewise for \(y'\)), with indices of \(x'\) and \(y'\) read modulo \(N\). Then for every \(k < N\), the coefficient of \(X^k\) in \(P_x P_y\) equals

\[\sum_{j \in \mathbb{Z}/N\mathbb{Z}} x'_j \, y'_{k - j}.\]

theorem fftPad_circular_coeff_eq_polynomial (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ (d + 1))) :
    (∑ j : ZMod (2 ^ (d + 1)), (fftPad d xs).ret.toArray.getD j.val 0 *
      (fftPad d ys).ret.toArray.getD ((k.val : ZMod (2 ^ (d + 1))) - j).val 0) =
      (fftPolynomial xs * fftPolynomial ys).coeff k.val

Uses 5 · Used by 2

Statement usesZero padding to twice the length · Polynomial of a coefficient vector

Proof usesCoefficients of the polynomial of a vector · Zero padding preserves the polynomial · Coefficients of a product of vector polynomials

Used byFFT linear convolution gives the product coefficients (Princeton sign) · FFT linear convolution gives the product coefficients (MIT/CLRS sign)

TheoremFFT linear convolution gives the product coefficients (Princeton sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{-2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), write \(P_x = \sum_{j < 2^d} x_j X^j\) and \(P_y = \sum_{j < 2^d} y_j X^j\), and let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then for every \(k < N\), the entry \(z_k\) is the coefficient of \(X^k\) in \(P_x P_y\).

theorem fftLinear_stdAddChar_neg_one_coeff (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ (d + 1))) :
    (fftLinear d (ZMod.stdAddChar (-1 : ZMod (2 ^ (d + 1)))) xs ys).ret[k.val] =
      (fftPolynomial xs * fftPolynomial ys).coeff k.val

Uses 7 · Used by 3

Statement usesFFT linear convolution · Polynomial of a coefficient vector

Proof usesFFT circular convolution · FFT circular convolution with root \(e^{-2\pi i/n}\) computes the cyclic convolution · Output of FFT linear convolution · Zero padding to twice the length · Zero padding turns cyclic convolution into the polynomial product

Used byThe last entry of FFT linear convolution is zero (Princeton sign) · FFT linear convolution computes the convolution sums (Princeton sign) · FFT linear convolution returns the product polynomial (Princeton sign)

TheoremFFT linear convolution computes the convolution sums (Princeton sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{-2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), extended by \(x_j = y_j = 0\) for \(j \ge 2^d\), let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then for every \(k < N\),

\[z_k = \sum_{j=0}^{k} x_j \, y_{k-j}.\]

theorem fftLinear_stdAddChar_neg_one_sum (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ (d + 1))) :
    (fftLinear d (ZMod.stdAddChar (-1 : ZMod (2 ^ (d + 1)))) xs ys).ret[k.val] =
      ∑ j ∈ Finset.range (k.val + 1),
        xs.toArray.getD j 0 * ys.toArray.getD (k.val - j) 0

Uses 4

Statement usesFFT linear convolution

Proof usesFFT linear convolution gives the product coefficients (Princeton sign) · Polynomial of a coefficient vector · Coefficients of a product of vector polynomials

TheoremFFT linear convolution returns the product polynomial (Princeton sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{-2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), write \(P_x = \sum_{j < 2^d} x_j X^j\) and \(P_y = \sum_{j < 2^d} y_j X^j\), and let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then \(\sum_{k < N} z_k X^k = P_x P_y\) as polynomials over \(\mathbb{C}\).

theorem fftPolynomial_fftLinear_stdAddChar_neg_one (d : Nat)
    (xs ys : Vector ℂ (2 ^ d)) :
    fftPolynomial (fftLinear d (ZMod.stdAddChar (-1 : ZMod (2 ^ (d + 1)))) xs ys).ret =
      fftPolynomial xs * fftPolynomial ys

Uses 5

Statement usesFFT linear convolution · Polynomial of a coefficient vector

Proof usesFFT linear convolution gives the product coefficients (Princeton sign) · Coefficients of the polynomial of a vector · Coefficients of a product beyond twice the length vanish

TheoremThe last entry of FFT linear convolution is zero (Princeton sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{-2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then the last entry \(z_{N-1}\) is \(0\).

theorem fftLinear_stdAddChar_neg_one_last (d : Nat) (xs ys : Vector ℂ (2 ^ d)) :
    (fftLinear d (ZMod.stdAddChar (-1 : ZMod (2 ^ (d + 1)))) xs ys).ret.toArray.getD
      (2 * 2 ^ d - 1) 0 = 0

Uses 4

Statement usesFFT linear convolution

Proof usesFFT linear convolution gives the product coefficients (Princeton sign) · Polynomial of a coefficient vector · The last coefficient of a doubled-length product vanishes

TheoremFFT linear convolution gives the product coefficients (MIT/CLRS sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), write \(P_x = \sum_{j < 2^d} x_j X^j\) and \(P_y = \sum_{j < 2^d} y_j X^j\), and let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then for every \(k < N\), the entry \(z_k\) is the coefficient of \(X^k\) in \(P_x P_y\).

theorem fftLinear_stdAddChar_one_coeff (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ (d + 1))) :
    (fftLinear d (ZMod.stdAddChar (1 : ZMod (2 ^ (d + 1)))) xs ys).ret[k.val] =
      (fftPolynomial xs * fftPolynomial ys).coeff k.val

Uses 7 · Used by 3

Statement usesFFT linear convolution · Polynomial of a coefficient vector

Proof usesFFT circular convolution · FFT circular convolution with root \(e^{2\pi i/n}\) computes the cyclic convolution · Output of FFT linear convolution · Zero padding to twice the length · Zero padding turns cyclic convolution into the polynomial product

Used byThe last entry of FFT linear convolution is zero (MIT/CLRS sign) · FFT linear convolution computes the convolution sums (MIT/CLRS sign) · FFT linear convolution returns the product polynomial (MIT/CLRS sign)

TheoremFFT linear convolution computes the convolution sums (MIT/CLRS sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), extended by \(x_j = y_j = 0\) for \(j \ge 2^d\), let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then for every \(k < N\),

\[z_k = \sum_{j=0}^{k} x_j \, y_{k-j}.\]

theorem fftLinear_stdAddChar_one_sum (d : Nat) (xs ys : Vector ℂ (2 ^ d))
    (k : Fin (2 ^ (d + 1))) :
    (fftLinear d (ZMod.stdAddChar (1 : ZMod (2 ^ (d + 1)))) xs ys).ret[k.val] =
      ∑ j ∈ Finset.range (k.val + 1),
        xs.toArray.getD j 0 * ys.toArray.getD (k.val - j) 0

Uses 4

Statement usesFFT linear convolution

Proof usesFFT linear convolution gives the product coefficients (MIT/CLRS sign) · Polynomial of a coefficient vector · Coefficients of a product of vector polynomials

TheoremFFT linear convolution returns the product polynomial (MIT/CLRS sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), write \(P_x = \sum_{j < 2^d} x_j X^j\) and \(P_y = \sum_{j < 2^d} y_j X^j\), and let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then \(\sum_{k < N} z_k X^k = P_x P_y\) as polynomials over \(\mathbb{C}\).

theorem fftPolynomial_fftLinear_stdAddChar_one (d : Nat)
    (xs ys : Vector ℂ (2 ^ d)) :
    fftPolynomial (fftLinear d (ZMod.stdAddChar (1 : ZMod (2 ^ (d + 1)))) xs ys).ret =
      fftPolynomial xs * fftPolynomial ys

Uses 5

Statement usesFFT linear convolution · Polynomial of a coefficient vector

Proof usesFFT linear convolution gives the product coefficients (MIT/CLRS sign) · Coefficients of the polynomial of a vector · Coefficients of a product beyond twice the length vanish

TheoremThe last entry of FFT linear convolution is zero (MIT/CLRS sign)#✓fully proved

Let \(d\) be a natural number, \(N = 2^{d+1}\) and \(\omega = e^{2\pi i/N}\). For vectors \(x, y \in \mathbb{C}^{2^d}\), let \(z \in \mathbb{C}^N\) be the output of the FFT linear convolution of \(x\) and \(y\) with root \(\omega\), which pads both vectors with zeros to length \(N\) and convolves them circularly by FFT. Then the last entry \(z_{N-1}\) is \(0\).

theorem fftLinear_stdAddChar_one_last (d : Nat) (xs ys : Vector ℂ (2 ^ d)) :
    (fftLinear d (ZMod.stdAddChar (1 : ZMod (2 ^ (d + 1)))) xs ys).ret.toArray.getD
      (2 * 2 ^ d - 1) 0 = 0

Uses 4

Statement usesFFT linear convolution

Proof usesFFT linear convolution gives the product coefficients (MIT/CLRS sign) · Polynomial of a coefficient vector · The last coefficient of a doubled-length product vanishes

TheoremInverse FFT after FFT at the positive root is the identity#✓fully proved

Let \(d\) be a natural number, \(N = 2^d\) and \(\omega = e^{2\pi i/N}\). For every vector \(x \in \mathbb{C}^N\), running the radix-two FFT with root \(\omega\) on \(x\) and then the inverse FFT with root \(\omega\) on its output returns \(x\).

theorem ifft_fft_stdAddChar_one (d : Nat) (xs : Vector ℂ (2 ^ d)) :
    (ifft d (ZMod.stdAddChar (1 : ZMod (2 ^ d)))
      (fft d (ZMod.stdAddChar (1 : ZMod (2 ^ d))) xs).ret).ret = xs

Uses 4

Statement usesRadix-two fast Fourier transform · Inverse FFT by conjugation

Proof usesThe radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Inverse FFT at the positive-sign root computes the normalized forward DFT

TheoremFFT after inverse FFT at the positive root is the identity#✓fully proved

Let \(d\) be a natural number, \(N = 2^d\) and \(\omega = e^{2\pi i/N}\). For every vector \(x \in \mathbb{C}^N\), running the inverse FFT with root \(\omega\) on \(x\) and then the radix-two FFT with root \(\omega\) on its output returns \(x\).

theorem fft_ifft_stdAddChar_one (d : Nat) (xs : Vector ℂ (2 ^ d)) :
    (fft d (ZMod.stdAddChar (1 : ZMod (2 ^ d)))
      (ifft d (ZMod.stdAddChar (1 : ZMod (2 ^ d))) xs).ret).ret = xs

Uses 4

Statement usesRadix-two fast Fourier transform · Inverse FFT by conjugation

Proof usesThe radix-two FFT with root \(e^{2\pi i/n}\), divided by \(n\), computes the inverse DFT · Inverse FFT at the positive-sign root computes the normalized forward DFT

90 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.