Fixed-point rounding: $|\rho(u)|\le|u|$ and $|\rho(u)-u|<\sqrt2\cdot2^{-p}$

Proved

IntMul.HvdH.rho_bounds

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

integer-multiplication

Let $p\ge0$ and let $\rho(u)=2^{-p}\rho_0(2^pu)$ be rounding towards zero to precision $p$ , as defined in IntMul_HvdH_FixedPoint. Then for every $u\in\mathbb C$ ,

|\rho(u)|\le|u|\qquad\text{and}\qquad|\rho(u)-u|<\sqrt2\cdot2^{-p}.

In particular $\rho$ maps the closed unit disc into the fixed-point unit disc $\tilde{\mathbb C}_\circ$ . These are the basic properties of $\rho$ stated in §2.2 of Harvey–van der Hoeven.

Preamble

import Definitions.Def_IntMul_HvdH_FixedPoint

Formal statement

namespace IntMul.HvdH
theorem rho_bounds (p : ℕ) (u : ℂ) :
    ‖rho p u‖ ≤ ‖u‖ ∧ ‖rho p u - u‖ < Real.sqrt 2 * ((2 : ℝ) ^ p)⁻¹ := 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, p. 9 (properties of rho)

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

Fixed-point rounding: ∣ρ(u)∣≤∣u∣|\rho(u)|\le|u|∣ρ(u)∣≤∣u∣ and ∣ρ(u)−u∣<2⋅2−p|\rho(u)-u|<\sqrt2\cdot2^{-p}∣ρ(u)−u∣<2​⋅2−p

Fixed-point rounding: $|\rho(u)|\le|u|$ and $|\rho(u)-u|<\sqrt2\cdot2^{-p}$