The normalised synthetic FFT is 1-Lipschitz

Proved

IntMul.HvdH.synG_lip

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

integer-multiplication

For $R=\mathbb C[y]/(y^r+1)$ and $t=2^e$ , the normalised synthetic transform $\mathcal G_t=\tfrac1t\,\widehat{\cdot}$ , computed by the radix-2 recursion synG, is $1$ -Lipschitz for the sup norm on coefficient arrays:

\|\mathcal G_t u-\mathcal G_t v\|_\infty\le\|u-v\|_\infty.

This is the norm bound $\|\mathcal G_t\|\le1$ used in Harvey–van der Hoeven §3.2.

Preamble

import Definitions.Def_IntMul_HvdH_SynFFT

Formal statement

namespace IntMul.HvdH
theorem synG_lip (r e : ℕ) : SupLip (synG r e) := 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, Lemma 3.2

View graph