Error of slice-wise tensor product approximations (Lemma 2.11)

Proved

IntMul.HvdH.tensor_error

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

integer-multiplication

Let $d\ge0$ . For each axis $i$ let $A_i$ be a one-dimensional map that is nonexpansive for the max-norm (as is any linear map of norm $\le1$ ). Let $\tilde A_i$ map the closed unit ball into itself and approximate $A_i$ there with error at most $e_i$ in every entry. Then for every array $x$ in the unit ball, the slice-wise tensor products (see IntMul_HvdH_SliceTensor) satisfy

\Bigl\|\Bigl(\bigotimes_i\tilde A_i\Bigr)x-\Bigl(\bigotimes_iA_i\Bigr)x\Bigr\|_\infty\le\sum_ie_i.

This is the error statement $\varepsilon(\tilde A)\le\sum_i\varepsilon(\tilde A_i)$ of Lemma 2.11 of Harvey–van der Hoeven.

Preamble

import Definitions.Def_IntMul_HvdH_SliceTensor

Formal statement

namespace IntMul.HvdH
theorem tensor_error {d : ℕ} (A Aa : Fin d → (ℕ → ℂ) → (ℕ → ℂ)) (e : Fin d → ℝ)
    (hA : ∀ i, ∀ (x y : ℕ → ℂ) (δ : ℝ), (∀ k, ‖x k - y k‖ ≤ δ) → ∀ j, ‖A i x j - A i y j‖ ≤ δ)
    (hAa : ∀ i (x : ℕ → ℂ), (∀ k, ‖x k‖ ≤ 1) → ∀ j, ‖Aa i x j‖ ≤ 1)
    (herr : ∀ i (x : ℕ → ℂ), (∀ k, ‖x k‖ ≤ 1) → ∀ j, ‖Aa i x j - A i x j‖ ≤ e i)
    (x : (Fin d → ℕ) → ℂ) (hx : ∀ j, ‖x j‖ ≤ 1) (j : Fin d → ℕ) :
    ‖tensorMap Aa x j - tensorMap A x j‖ ≤ ∑ i, e i := 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.7, Lemma 2.11 (tensor products)

View graph