Prove2Me

Fixed-point product error (Lemma 2.4 / Corollary 2.10)

Proved
IntMul.HvdH.fp_mul_error

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

integer-multiplication

Let p≥0p\ge0, let u,v∈Cu,v\in\mathbb C and approximations u~,v~\tilde u,\tilde v with ∣u∣≤1|u|\le1 and ∣v~∣≤1|\tilde v|\le1, and suppose 2p∣u~−u∣≤εu2^p|\tilde u-u|\le\varepsilon_u and 2p∣v~−v∣≤εv2^p|\tilde v-v|\le\varepsilon_v. Then the rounded product w~=ρ(u~v~)\tilde w=\rho(\tilde u\tilde v) (rounding towards zero to precision pp, see IntMul_HvdH_FixedPoint) satisfies

2p ∣w~−uv∣<εu+εv+2.2^p\,|\tilde w-uv|<\varepsilon_u+\varepsilon_v+2.

This is Corollary 2.10 of Harvey–van der Hoeven (combining Lemma 2.4 and Lemma 2.9).

Preamble
import Definitions.Def_IntMul_HvdH_FixedPoint
Formal statement
namespace IntMul.HvdH
theorem fp_mul_error (p : ℕ) (u v ut vt : ℂ) (hu : ‖u‖ ≤ 1) (hvt : ‖vt‖ ≤ 1)
    (eu ev : ℝ) (hut : (2 : ℝ) ^ p * ‖ut - u‖ ≤ eu) (hvt' : (2 : ℝ) ^ p * ‖vt - v‖ ≤ ev) :
    (2 : ℝ) ^ p * ‖rho p (ut * vt) - u * v‖ < eu + ev + 2 := 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.6 (Lemma 2.4, Corollary 2.10)
Human review

  • Endorsed by Shuze Chen · Oct 24, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 24, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph