Prove2Me

Fixed-point scaling error (Lemma 2.2): ε(v~)<2c ε(u~)+3\varepsilon(\tilde v)<2c\,\varepsilon(\tilde u)+3

Proved
IntMul.HvdH.scaleFP_bound

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

integer-multiplication

Let p≥0p\ge0, let c≥1c\ge1 be an integer, and let u∈Cu\in\mathbb C with ∣u∣≤1/c|u|\le 1/c, so that v:=cuv:=cu lies in the unit disc. Let u~∈C\tilde u\in\mathbb C be any approximation of uu, and let v~\tilde v be the output of the scaling procedure scaleFP (Lemma 2.2: take cu~c\tilde u if it lies in the unit disc, otherwise renormalise by b=⌈2p∣cu~∣⌉b=\lceil2^p|c\tilde u|\rceil and round). Then ∣v~∣≤1|\tilde v|\le1, and the errors ε(v~)=2p∣v~−v∣\varepsilon(\tilde v)=2^p|\tilde v-v| and ε(u~)=2p∣u~−u∣\varepsilon(\tilde u)=2^p|\tilde u-u| satisfy

ε(v~)<2c ε(u~)+3.\varepsilon(\tilde v)<2c\,\varepsilon(\tilde u)+3 .

This is the error statement of Lemma 2.2 of Harvey–van der Hoeven, used for example in the final scaling step of an inverse FFT.

Preamble
import Definitions.Def_IntMul_HvdH_FixedPoint
Formal statement
namespace IntMul.HvdH
theorem scaleFP_bound (p c : ℕ) (hc : 1 ≤ c) (u ũ : ℂ) (hu : ‖u‖ ≤ (c : ℝ)⁻¹) :
    ‖scaleFP p c ũ‖ ≤ 1 ∧
      (2 : ℝ) ^ p * ‖scaleFP p c ũ - c * u‖ < 2 * c * ((2 : ℝ) ^ p * ‖ũ - u‖) + 3 := 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, Section 2.2, Lemma 2.2 (error bound)

View graph