Tensor products of 1-Lipschitz maps are 1-Lipschitz

Proved

IntMul.HvdH.lip_tensor

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

integer-multiplication

If each one-dimensional map $A_i$ ( $i<d$ ) is $1$ -Lipschitz for the sup norm (SupLip, see IntMul_HvdH_FPApprox), then so is the slice-by-slice tensor product $\bigotimes_iA_i$ (tensorMap). For linear maps this is $\|\bigotimes_iA_i\|\le1$ when every $\|A_i\|\le1$ .

Preamble

import Definitions.Def_IntMul_HvdH_FPApprox

Formal statement

namespace IntMul.HvdH
theorem lip_tensor {d : ℕ} (A : Fin d → (ℕ → ℂ) → (ℕ → ℂ)) (hL : ∀ i, SupLip (A i)) :
    SupLip (tensorMap A) := 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.7

View graph