Prove2Me

Error of a composition of approximate linear maps (Corollary 2.8)

Proved
IntMul.HvdH.error_composition

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

integer-multiplication

Let A:U→VA:U\to V and B:V→WB:V\to W be continuous C\mathbb C-linear maps with ∥B∥≤1\|B\|\le1. Let A~:U→V\tilde A:U\to V map a set SS into a set TT with ∥A~u−Au∥≤εA\|\tilde Au-Au\|\le\varepsilon_A on SS, and let B~:V→W\tilde B:V\to W satisfy ∥B~v−Bv∥≤εB\|\tilde Bv-Bv\|\le\varepsilon_B on TT. Then for all u∈Su\in S,

∥B~A~u−BAu∥≤εB+εA.\|\tilde B\tilde Au-BAu\|\le\varepsilon_B+\varepsilon_A.

This is Corollary 2.8 of Harvey–van der Hoeven, with S,TS,T the fixed-point unit balls.

Preamble
import Mathlib
Formal statement
namespace IntMul.HvdH
theorem error_composition {U V W : Type*} [NormedAddCommGroup U] [NormedSpace ℂ U]
    [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W]
    (A : U →L[ℂ] V) (B : V →L[ℂ] W) (hB : ‖B‖ ≤ 1)
    (Aa : U → V) (Bb : V → W) (S : Set U) (T : Set V) (eA eB : ℝ)
    (hAaT : ∀ u ∈ S, Aa u ∈ T) (hAa : ∀ u ∈ S, ‖Aa u - A u‖ ≤ eA)
    (hBb : ∀ v ∈ T, ‖Bb v - B v‖ ≤ eB) :
    ∀ u ∈ S, ‖Bb (Aa u) - B (A u)‖ ≤ eB + eA := 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

View graph