Convolution theorem for the DFT on $\mathbb Z/N$

Proved

IntMul.HvdH.dft_cyclic_conv

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

fourier-analysisinteger-multiplication

Let $N\ge1$ and let $u,v:\mathbb Z/N\to\mathbb C$ . Write $\hat u(k)=\sum_{j\in\mathbb Z/N} e^{-2\pi i jk/N}u_j$ for the (unnormalised) discrete Fourier transform, as in Mathlib's ZMod.dft, and $(u*v)_m=\sum_{j\in\mathbb Z/N}u_j\,v_{m-j}$ for cyclic convolution. Then for every $k$ ,

\widehat{u*v}(k)=\hat u(k)\,\hat v(k).

This is equation (2.1) / §2.4 of Harvey–van der Hoeven: it is how the $O(n\log n)$ algorithm turns a cyclic convolution (an integer product after chunking) into pointwise products of DFTs.

Preamble

import Mathlib

Formal statement

namespace IntMul.HvdH
theorem dft_cyclic_conv {N : ℕ} [NeZero N] (u v : ZMod N → ℂ) (k : ZMod N) :
    ZMod.dft (fun m => ∑ j, u j * v (m - j)) k = ZMod.dft u k * ZMod.dft v k := 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 5.3

View graph

Convolution theorem for the DFT on Z/N\mathbb Z/NZ/N

Convolution theorem for the DFT on $\mathbb Z/N$