Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 4.5 — ∥S∥<1+α−1\|\mathcal S\|<1+\alpha^{-1}∥S∥<1+α−1

Proved
IntMul.HvdH.lemma_4_5

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

harmonic-analysisoperator-norm

Let sss and t>st>st>s be positive integers with gcd⁡(s,t)=1\gcd(s,t)=1gcd(s,t)=1, and let α>0\alpha>0α>0. The resampling map S:Cs→Ct\mathcal S:\mathbb C^s\to\mathbb C^tS:Cs→Ct,

(Su)k=α−1∑j∈Ze−πα−2s2(k/t−j/s)2uj mod s,(\mathcal Su)_k=\alpha^{-1}\sum_{j\in\mathbb Z}e^{-\pi\alpha^{-2}s^2(k/t-j/s)^2}u_{j\bmod s},(Su)k​=α−1j∈Z∑​e−πα−2s2(k/t−j/s)2ujmods​,

satisfies

∥S∥<1+α−1,\|\mathcal S\|<1+\alpha^{-1},∥S∥<1+α−1,

where ∥⋅∥\|\cdot\|∥⋅∥ is the operator norm with respect to the supremum norms on Cs\mathbb C^sCs and Ct\mathbb C^tCt.

This bound keeps the forward resampling step numerically stable, with growth by at most a constant factor.

Preamble
import Mathlib
import Definitions.Def_IntMul_HvdH_Resampling
Formal statement
namespace IntMul.HvdH

theorem lemma_4_5 (s t : ℕ) [NeZero s] [NeZero t] (hst : s < t) (hcop : Nat.Coprime s t)
    (α : ℝ) (hα : 0 < α) :
    ‖resS s t α‖ < 1 + α⁻¹ := 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, Lemma 4.5, p. 26 (setting of §4.1; norms of §2.2, §2.6)
Read-back

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

Statement (IntMul.HvdH.lemma_4_5). Let s,ts, ts,t be natural numbers with s≠0s \neq 0s=0 and t≠0t \neq 0t=0, with s<ts < ts<t, and with gcd⁡(s,t)=1\gcd(s,t) = 1gcd(s,t)=1. Let α\alphaα be a real number with α>0\alpha > 0α>0. Then the operator norm of the linear map S=Ss,t,α:Cs→Ct\mathcal{S} = \mathcal{S}_{s,t,\alpha} : \mathbb{C}^s \to \mathbb{C}^tS=Ss,t,α​:Cs→Ct defined below satisfies the strict inequality

∥S∥  <  1+α−1.\|\mathcal{S}\| \;<\; 1 + \alpha^{-1}.∥S∥<1+α−1.

The spaces and the norm. Cn\mathbb{C}^nCn here means the space of functions Z/nZ→C\mathbb{Z}/n\mathbb{Z} \to \mathbb{C}Z/nZ→C, indices taken as residues 0,1,…,n−10,1,\dots,n-10,1,…,n−1. Each such space carries the supremum norm ∥u∥=max⁡0≤j<n∣uj∣\|u\| = \max_{0 \le j < n} |u_j|∥u∥=max0≤j<n​∣uj​∣ (with ∣⋅∣|\cdot|∣⋅∣ the complex modulus). The norm ∥S∥\|\mathcal{S}\|∥S∥ is the operator norm of S\mathcal{S}S as a map between these sup-normed spaces, i.e. ∥S∥=sup⁡{∥Su∥∞:∥u∥∞≤1}\|\mathcal{S}\| = \sup\{\|\mathcal{S}u\|_\infty : \|u\|_\infty \le 1\}∥S∥=sup{∥Su∥∞​:∥u∥∞​≤1} (the ℓ∞→ℓ∞\ell^\infty \to \ell^\inftyℓ∞→ℓ∞ operator norm). For a matrix AAA this equals the maximum absolute row sum max⁡k∑r∣Ak,r∣\max_k \sum_r |A_{k,r}|maxk​∑r​∣Ak,r​∣.

The map S\mathcal{S}S, unfolded. S\mathcal{S}S is the linear map given by the t×st \times st×s complex matrix AAA, with rows indexed by k∈{0,…,t−1}k \in \{0,\dots,t-1\}k∈{0,…,t−1} and columns by r∈{0,…,s−1}r \in \{0,\dots,s-1\}r∈{0,…,s−1}, whose entries are the real numbers (viewed as complex numbers)

Ak,r  =  ∑m∈Zα−1exp⁡ ⁣(−π α−2 s2(kt−r+mss)2),A_{k,r} \;=\; \sum_{m \in \mathbb{Z}} \alpha^{-1} \exp\!\Big(-\pi\,\alpha^{-2}\, s^2 \Big(\frac{k}{t} - \frac{r + m s}{s}\Big)^{2}\Big),Ak,r​=m∈Z∑​α−1exp(−πα−2s2(tk​−sr+ms​)2),

so that (Su)k=∑r=0s−1Ak,r ur(\mathcal{S}u)_k = \sum_{r=0}^{s-1} A_{k,r}\, u_r(Su)k​=∑r=0s−1​Ak,r​ur​. Equivalently, writing j=r+msj = r + msj=r+ms and reading uju_juj​ as uj mod su_{j \bmod s}ujmods​,

(Su)k  =  α−1∑j∈Ze−πα−2s2(k/t−j/s)2 uj mod s,0≤k<t.(\mathcal{S}u)_k \;=\; \alpha^{-1} \sum_{j \in \mathbb{Z}} e^{-\pi \alpha^{-2} s^2 (k/t - j/s)^2}\, u_{j \bmod s}, \qquad 0 \le k < t .(Su)k​=α−1j∈Z∑​e−πα−2s2(k/t−j/s)2ujmods​,0≤k<t.

The sum over m∈Zm \in \mathbb{Z}m∈Z is an unconditional infinite sum; by convention it would be assigned the value 000 if it failed to converge, but for α>0\alpha > 0α>0 the Gaussian terms are summable, so it is the genuine series value. All entries Ak,rA_{k,r}Ak,r​ are strictly positive reals. Consequently the claim is equivalent to

max⁡0≤k<t  α−1∑j∈Zexp⁡ ⁣(−πα2(j−skt)2)  <  1+α−1.\max_{0 \le k < t} \; \alpha^{-1} \sum_{j \in \mathbb{Z}} \exp\!\Big(-\frac{\pi}{\alpha^{2}}\Big(j - \frac{sk}{t}\Big)^{2}\Big) \;<\; 1 + \alpha^{-1}.0≤k<tmax​α−1j∈Z∑​exp(−α2π​(j−tsk​)2)<1+α−1.

Binders and hypotheses.

  • s,t∈Ns, t \in \mathbb{N}s,t∈N, each assumed nonzero (so s≥1s \ge 1s≥1; together with s<ts < ts<t this forces t≥2t \ge 2t≥2).
  • s<ts < ts<t (strict).
  • sss and ttt coprime. This includes s=1s = 1s=1 with any t≥2t \ge 2t≥2.
  • α∈R\alpha \in \mathbb{R}α∈R with α>0\alpha > 0α>0 (strict). There is no upper or lower bound on α\alphaα beyond positivity; both α→0+\alpha \to 0^+α→0+ and arbitrarily large α\alphaα are covered.

Edge cases and remarks. The hypotheses are jointly satisfiable (e.g. s=1s=1s=1, t=2t=2t=2, α=1\alpha=1α=1), so the statement is not vacuous. The hypotheses s<ts<ts<t and gcd⁡(s,t)=1\gcd(s,t)=1gcd(s,t)=1 do not enter the definition of S\mathcal{S}S; they only restrict which pairs (s,t)(s,t)(s,t) the bound is asserted for. The row k=0k = 0k=0 is included, where the row sum is α−1∑j∈Ze−πj2/α2\alpha^{-1}\sum_{j\in\mathbb{Z}} e^{-\pi j^2/\alpha^2}α−1∑j∈Z​e−πj2/α2. The conclusion is a strict inequality (<<<), not ≤\le≤.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me