Fixed-point complex product stays in the unit disc

Proved

IntMul.HvdH.mulZ_disc

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

integer-multiplication

Let $p\ge0$ and let $a,b\in\mathbb Z[i]$ with $|a|,|b|\le 2^p$ . The fixed-point product mulZ p a b $=\rho_0(ab/2^p)$ , which rounds the real and imaginary parts of $ab/2^p$ towards zero, satisfies

|\,\mathrm{mulZ}_p(a,b)\,|\le 2^p .

So fixed-point multiplication at precision $p$ maps the closed unit polydisc (in units of $2^{-p}$ ) into itself, as in §2.3 of Harvey–van der Hoeven.

Preamble

import Definitions.Def_IntMul_HvdH_ConvC

Formal statement

namespace IntMul.HvdH
theorem mulZ_disc (p : ℕ) (a b : ℤ × ℤ) (ha : ‖gC a‖ ≤ 2 ^ p) (hb : ‖gC b‖ ≤ 2 ^ p) :
    ‖gC (mulZ p a b)‖ ≤ 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, §2.3, Lemma 2.4

View graph