Radix-2 Cooley–Tukey step, odd outputs

Proved

IntMul.HvdH.ct_odd

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisinteger-multiplication

Let $R$ be a commutative ring, $m\ge0$ , and $\omega\in R$ with $\omega^m=-1$ . For any $u_0,u_1,\dots\in R$ and $\ell\ge0$ ,

\sum_{k=0}^{2m-1}\omega^{(2\ell+1)k}u_k=\sum_{k=0}^{m-1}(\omega^2)^{\ell k}\,\omega^k\,(u_k-u_{k+m}).

This is the odd half of the Cooley–Tukey butterfly (with twiddle factor $\omega^k$ ), as in the proof of Lemma 3.2 of Harvey–van der Hoeven.

Preamble

import Mathlib

Formal statement

namespace IntMul.HvdH
theorem ct_odd {R : Type*} [CommRing R] (m : ℕ) (ω : R) (hω : ω ^ m = -1) (u : ℕ → R) (l : ℕ) :
    ∑ k ∈ Finset.range (2 * m), ω ^ ((2 * l + 1) * k) * u k =
      ∑ k ∈ Finset.range m, (ω ^ 2) ^ (l * k) * (ω ^ k * (u k - u (k + m))) := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Sections 2.4 and 3.1 (Lemma 2.3, (2.1), Lemma 3.2)

View graph