Theorem 4.2 — resampling identity $\mathcal T\mathcal P_s\mathcal F_s=\mathcal P_t\mathcal F_t\mathcal S$

Proved

IntMul.HvdH.theorem_4_2

by avi · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-transformharmonic-analysis

Let $s$ and $t>s$ be positive integers with $\gcd(s,t)=1$ , and let $\alpha>0$ . Let $\mathcal F_n$ be the normalized DFT of length $n$ , let $\mathcal S,\mathcal T:\mathbb C^s\to\mathbb C^t$ be the Gaussian resampling maps

(\mathcal Su)_k=\alpha^{-1}\sum_{j\in\mathbb Z}e^{-\pi\alpha^{-2}s^2(k/t-j/s)^2}u_j,\qquad(\mathcal Tu)_k=\sum_{j\in\mathbb Z}e^{-\pi\alpha^2t^2(k/t-j/s)^2}u_j,

and let $(\mathcal P_su)_j=u_{tj}$ and $(\mathcal P_tu)_k=u_{-sk}$ , where indices are read modulo $s$ and modulo $t$ respectively. Then

\mathcal T\,\mathcal P_s\,\mathcal F_s=\mathcal P_t\,\mathcal F_t\,\mathcal S .

This identity expresses a DFT of length $s$ in terms of a DFT of the larger length $t$ . It is how Harvey and van der Hoeven replace transforms of prime length by transforms whose lengths are powers of two.

Preamble

import Mathlib
import Definitions.Def_IntMul_HvdH_Resampling

Formal statement

namespace IntMul.HvdH

theorem theorem_4_2 (s t : ℕ) [NeZero s] [NeZero t] (hst : s < t) (hcop : Nat.Coprime s t)
    (α : ℝ) (hα : 0 < α) :
    (resT s t α).comp ((permS s t).comp (dft s)) =
      (permT s t).comp ((dft t).comp (resS s t α)) := by sorry

end IntMul.HvdH

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2) (2021) 563-617, https://doi.org/10.4007/annals.2021.193.2.4 (preprint https://hal.science/hal-02070778v2), §4.1, Theorem 4.2, p. 24 (setting of §4.1: s < t positive, gcd(s,t)=1, alpha in (0,inf))

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back of IntMul.HvdH.theorem_4_2.

Data and hypotheses. Let $s, t$ be natural numbers with $s \neq 0$ and $t \neq 0$ , with $s < t$ (strict), and with $\gcd(s,t) = 1$ . Let $\alpha$ be a real number with $\alpha > 0$ . No other assumptions are made. Vectors in $\mathbb{C}^n$ are functions $\mathbb{Z}/n\mathbb{Z} \to \mathbb{C}$ ; for a residue $a \in \mathbb{Z}/n\mathbb{Z}$ , $\bar a \in \{0,\dots,n-1\}$ denotes its least non-negative representative, and indices are always read mod $n$ .

Maps involved (all are $\mathbb{C}$ -linear, automatically continuous, and given by explicit matrices):

DFT $\mathcal{F}_n : \mathbb{C}^n \to \mathbb{C}^n$ (used for $n = s$ and $n = t$ ):

(\mathcal{F}_n u)_j = \frac{1}{n}\sum_{k=0}^{n-1} \exp\!\Big(\frac{-2\pi i\, \bar j\, k}{n}\Big)\, u_k .

Note the normalization factor $1/n$ (not $1/\sqrt n$ ) and the minus sign in the exponent.

Permutation $\mathcal{P}_s : \mathbb{C}^s \to \mathbb{C}^s$ : $(\mathcal{P}_s u)_j = u_{t j \bmod s}$ (the product $t\cdot j$ computed in $\mathbb{Z}/s\mathbb{Z}$ ).
Permutation $\mathcal{P}_t : \mathbb{C}^t \to \mathbb{C}^t$ : $(\mathcal{P}_t u)_k = u_{-s k \bmod t}$ .
Resampling map $\mathcal{S} : \mathbb{C}^s \to \mathbb{C}^t$ : for $k \in \mathbb{Z}/t\mathbb{Z}$ ,

(\mathcal{S}u)_k = \sum_{r=0}^{s-1}\Big[\sum_{m\in\mathbb{Z}} \alpha^{-1}\exp\!\Big(-\pi\,\alpha^{-2} s^2\Big(\frac{\bar k}{t} - \frac{r + m s}{s}\Big)^{2}\Big)\Big]\, u_r .

Resampling map $\mathcal{T} : \mathbb{C}^s \to \mathbb{C}^t$ : for $k \in \mathbb{Z}/t\mathbb{Z}$ ,

(\mathcal{T}u)_k = \sum_{r=0}^{s-1}\Big[\sum_{m\in\mathbb{Z}} \exp\!\Big(-\pi\,\alpha^{2} t^2\Big(\frac{\bar k}{t} - \frac{r + m s}{s}\Big)^{2}\Big)\Big]\, u_r .

In both resampling maps the inner sum over $m \in \mathbb{Z}$ is an unconditional (tsum) sum, which by convention would be $0$ if the series were not summable; here, since $\alpha > 0$ and $s, t \ge 1$ , the summands are Gaussian in $m$ with strictly positive decay rate, so the series converge and the bracketed matrix entries are genuine positive reals. Equivalently, $(\mathcal{S}u)_k = \alpha^{-1}\sum_{j\in\mathbb{Z}} e^{-\pi\alpha^{-2}s^2(\bar k/t - j/s)^2}\,u_{j \bmod s}$ and $(\mathcal{T}u)_k = \sum_{j\in\mathbb{Z}} e^{-\pi\alpha^{2}t^2(\bar k/t - j/s)^2}\,u_{j \bmod s}$ .

Conclusion. As maps $\mathbb{C}^s \to \mathbb{C}^t$ (i.e. for every $u \in \mathbb{C}^s$ ), the following exact identity holds:

\mathcal{T}\circ\mathcal{P}_s\circ\mathcal{F}_s \;=\; \mathcal{P}_t\circ\mathcal{F}_t\circ\mathcal{S}.

The order of application is: on the left, first the $s$ -point DFT, then the permutation $\mathcal{P}_s$ , then $\mathcal{T}$ ; on the right, first $\mathcal{S}$ , then the $t$ -point DFT, then the permutation $\mathcal{P}_t$ . Written out entrywise, for every $u \in \mathbb{C}^s$ and every $k \in \mathbb{Z}/t\mathbb{Z}$ :

\sum_{r=0}^{s-1} \mathcal{T}_{k,r}\cdot\frac{1}{s}\sum_{q=0}^{s-1} e^{-2\pi i\,\overline{(t r \bmod s)}\, q/s}\,u_q \;=\; \frac{1}{t}\sum_{p=0}^{t-1} e^{-2\pi i\,\overline{(-s k \bmod t)}\,p/t}\,(\mathcal{S}u)_p ,

where $\mathcal{T}_{k,r}$ is the bracketed entry of $\mathcal{T}$ above. This is an equality, not an approximation or bound.

Edge cases and remarks. The hypotheses are satisfiable (e.g. $s = 1$ , $t = 2$ , any $\alpha > 0$ ), so the statement is not vacuous. The case $s = 1$ is included (then $\mathcal{F}_1$ and $\mathcal{P}_1$ are the identity on $\mathbb{C}^1$ and $t \ge 2$ is arbitrary); since $s < t$ , always $t \ge 2$ . The coprimality hypothesis ensures $\mathcal{P}_s$ and $\mathcal{P}_t$ are genuine permutations, though the maps are defined regardless. The source file also defines further objects (nearest-integer rounding, $\beta_\ell$ , the row-deletion map, the diagonal map, $\mathcal{N}$ , $\mathcal{E}$ , $\theta$ ), none of which appear in this theorem.

Human review

Endorsed by wurtle · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by avi · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 4.2 — resampling identity TPsFs=PtFtS\mathcal T\mathcal P_s\mathcal F_s=\mathcal P_t\mathcal F_t\mathcal STPs​Fs​=Pt​Ft​S

Theorem 4.2 — resampling identity $\mathcal T\mathcal P_s\mathcal F_s=\mathcal P_t\mathcal F_t\mathcal S$