Prove2Me

Fixed-point approximation B~\tilde{\mathcal B} of the inverse resampling map (Harvey–van der Hoeven Proposition 4.7(ii))

Definition
IntMul_HvdH_BApprox

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

integer-multiplication

The computable map B~=P~s−1D~′J~′C~P~t\tilde{\mathcal B}=\tilde P_s^{-1}\tilde{\mathcal D}'\tilde{\mathcal J}'\tilde{\mathcal C}\tilde P_t from the proof of Proposition 4.7(ii) of Harvey–van der Hoeven. It approximates

B=Ps−1D′J′CPt:Ct→Cs.\mathcal B=P_s^{-1}\mathcal D'\mathcal J'\mathcal CP_t:\mathbb C^t\to\mathbb C^s.

The maps P~t\tilde P_t, C~\tilde{\mathcal C} and P~s−1\tilde P_s^{-1} only rearrange data. The vector entries 0,…,n−10,\dots,n-1 of V:N→Z[i]V:\mathbb N\to\mathbb Z[i] hold a vector of Cn\mathbb C^n.

  • ptPerm s t V k =V−sk mod t=V_{-sk\bmod t}.
  • cSel s t V ℓ =V[tℓ′/s]=V_{[t\ell'/s]} with ℓ′=ℓ mod s\ell'=\ell\bmod s and [x]=⌊x+1/2⌋[x]=\lfloor x+1/2\rfloor. The output is ss-periodic.
  • psInvPerm s t W j =Wt−1j mod s=W_{t^{-1}j\bmod s}.
  • Bapprox p s t α V composes these with Japprox (Lemma 4.12) and Dapprox (Lemma 4.8).
Definition code
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_DiagApprox

/-! The fixed-point approximation `B̃ = P̃_s⁻¹ D̃' J̃' C̃ P̃_t` of the map `B` in Gaussian resampling
(Harvey–van der Hoeven Proposition 4.7(ii)). Gaussian integers are pairs `(re, im) : ℤ × ℤ`, and
a fixed-point vector of precision `p` is `U : ℕ → ℤ × ℤ` standing for `2^{-p} U`; a vector in
`ℂ^n` is stored in the entries `0, …, n - 1`. -/

namespace IntMul.HvdH

/-- `(P̃_t V)_k = V_{-sk mod t}`. -/
def ptPerm (s t : ℕ) (V : ℕ → ℤ × ℤ) (k : ℕ) : ℤ × ℤ :=
  V (-((s : ZMod t) * (k : ZMod t))).val

/-- `(C̃ V)_ℓ = V_{round(tℓ'/s) mod t}` with `ℓ' = ℓ mod s` (the output is `s`-periodic). -/
def cSel (s t : ℕ) (V : ℕ → ℤ × ℤ) (l : ℕ) : ℤ × ℤ :=
  V ((((2 * t * (l % s) + s) / (2 * s) : ℕ) : ZMod t)).val

/-- `(P̃_s⁻¹ W)_j = W_{t⁻¹ j mod s}`. -/
def psInvPerm (s t : ℕ) (W : ℕ → ℤ × ℤ) (j : ℕ) : ℤ × ℤ :=
  W ((t : ZMod s)⁻¹ * (j : ZMod s)).val

/-- `B̃ = P̃_s⁻¹ D̃' J̃' C̃ P̃_t` (Lemmas 4.8 and 4.12 and data rearrangements). -/
def Bapprox (p s t α : ℕ) (V : ℕ → ℤ × ℤ) : ℕ → ℤ × ℤ :=
  psInvPerm s t (Dapprox p s t α (Japprox p s t α (cSel s t (ptPerm s t V))))

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, Proposition 4.7

View graph