Prove2Me

Zero-padded cyclic convolution equals linear convolution

Proved
IntMul.HvdH.cyclic_conv_eq_linear

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

fourier-analysisinteger-multiplication

Let RR be a commutative ring and let u,v:N→Ru,v:\mathbb N\to R vanish at every index ≥n\ge n. If N≥2n−1N\ge 2n-1, then the cyclic convolution of length NN of the zero-padded vectors equals the ordinary (acyclic) convolution: for every 0≤k<N0\le k<N,

∑j∈Z/Nujˉ vk−j‾=∑i=0kui vk−i,\sum_{j\in\mathbb Z/N}u_{\bar j}\,v_{\overline{k-j}}=\sum_{i=0}^{k}u_i\,v_{k-i},

where xˉ∈{0,…,N−1}\bar x\in\{0,\dots,N-1\} is the canonical representative of x∈Z/Nx\in\mathbb Z/N.

This is the standard zero-padding step that lets an integer (or polynomial) product be computed by a cyclic convolution, as in §5.3 of Harvey–van der Hoeven.

Preamble
import Mathlib
Formal statement
namespace IntMul.HvdH
theorem cyclic_conv_eq_linear {R : Type*} [CommRing R] {N n : ℕ} [NeZero N]
    (hN : 2 * n ≤ N + 1) (u v : ℕ → R) (hu : ∀ i, n ≤ i → u i = 0) (hv : ∀ i, n ≤ i → v i = 0)
    (k : ℕ) (hk : k < N) :
    ∑ j : ZMod N, u j.val * v ((k : ZMod N) - j).val =
      ∑ i ∈ Finset.range (k + 1), u i * v (k - i) := 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