Prove2Me

Error propagation through an approximate bilinear map (Lemma 2.9)

Proved
IntMul.HvdH.bilinear_error_propagation

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

integer-multiplication

Let A:U×V→WA:U\times V\to W be a continuous C\mathbb C-bilinear map with ∥A∥≤1\|A\|\le1 and let A~\tilde A be any function U×V→WU\times V\to W. Let ∥u∥≤1\|u\|\le1, ∥v~∥≤1\|\tilde v\|\le1, ∥A~(u~,v~)−A(u~,v~)∥≤εA\|\tilde A(\tilde u,\tilde v)-A(\tilde u,\tilde v)\|\le\varepsilon_A, ∥u~−u∥≤εu\|\tilde u-u\|\le\varepsilon_u and ∥v~−v∥≤εv\|\tilde v-v\|\le\varepsilon_v. Then

∥A~(u~,v~)−A(u,v)∥≤εA+εu+εv.\|\tilde A(\tilde u,\tilde v)-A(u,v)\|\le\varepsilon_A+\varepsilon_u+\varepsilon_v.

This is Lemma 2.9 of Harvey–van der Hoeven.

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