Prove2Me

Error propagation through an approximate linear map (Lemma 2.7)

Proved
IntMul.HvdH.error_propagation

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

integer-multiplication

Let A:V→WA:V\to W be a continuous C\mathbb C-linear map between normed spaces with ∥A∥≤1\|A\|\le1, and let A~:V→W\tilde A:V\to W be any function. If ∥A~v~−Av~∥≤εA\|\tilde A\tilde v-A\tilde v\|\le\varepsilon_A and ∥v~−v∥≤εv\|\tilde v-v\|\le\varepsilon_v, then

∥A~v~−Av∥≤εA+εv.\|\tilde A\tilde v-Av\|\le\varepsilon_A+\varepsilon_v.

This is Lemma 2.7 of Harvey–van der Hoeven (errors measured in units of 2−p2^{-p} there).

Preamble
import Mathlib
Formal statement
namespace IntMul.HvdH
theorem error_propagation {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W]
    (A : V →L[ℂ] W) (hA : ‖A‖ ≤ 1) (Aa : V → W) (v vt : V) (eA ev : ℝ)
    (hAa : ‖Aa vt - A vt‖ ≤ eA) (hv : ‖vt - v‖ ≤ ev) : ‖Aa vt - A v‖ ≤ eA + ev := 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