The Duhamel bound: unitary groups of nearby generators stay close

Category: 1-Mathlib (CSD-free upstream candidates).

For skew-Hermitian generators C, A on a finite-dimensional Hilbert space,

‖exp (t • C) − exp (t • A)‖ ≤ |t| · ‖C − A‖

in the L2 operator norm. The classical Duhamel-formula estimate, here proved without integrals: the interpolant φ(s) = exp (s • C) · exp ((t−s) • A) has endpoints exp (t • C) and exp (t • A), its derivative is exp (s • C) · (C − A) · exp ((t−s) • A) — norm at most ‖C − A‖, the two exponential factors being unitary — and the mean-value inequality (Convex.norm_image_sub_le_of_norm_hasDerivWithin_le) does the rest.

This is the quantitative engine of A5 ((ε,T)-projectability): a Hamiltonian ε-close in operator norm to a sector-projectable one generates dynamics that the sector dynamics shadows to within ε·T over the time window [−T, T]. Consumed by SigmaLayer/ApproxProjectability.lean.

Provenance

Staged as upstream Mathlib material; no CsdLean4-namespace content beyond the Matrix.StoneC1 unitarity input. Generalized 2026-08-07 from Fin n to an arbitrary finite index (the CV pricing route, CV-9, needs it at FieldConfig K N): every ingredient — exp_conjTranspose, exp_add_of_commute, hasDerivAt_exp_smul_const, the scoped C*-instances, the mean-value inequality — is index-generic, so the unitarity input is inlined and [NeZero n] becomes [Nonempty m].

theorem Matrix.conjTranspose_real_smul_skew {m : Type u_1} {A : Matrix m m ℂ} (hA : A.conjTranspose = -A) (s : ℝ) : (s • A).conjTranspose = -(s • A)

Real scaling preserves skew-Hermiticity.

theorem Matrix.l2_opNorm_exp_smul_skew {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] (A : Matrix m m ℂ) (hA : A.conjTranspose = -A) (t : ℝ) : ‖NormedSpace.exp (t • A)‖ = 1

A skew-Hermitian generator exponentiates to a matrix of unit L2 operator norm — it is unitary, and the L2 operator norm is a C*-norm.

theorem Matrix.norm_exp_smul_sub_exp_smul_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] (C A : Matrix m m ℂ) (hC : C.conjTranspose = -C) (hA : A.conjTranspose = -A) (t : ℝ) : ‖NormedSpace.exp (t • C) - NormedSpace.exp (t • A)‖ ≤ |t| * ‖C - A‖

The Duhamel bound. For skew-Hermitian generators C, A, ‖exp (t • C) − exp (t • A)‖ ≤ |t| · ‖C − A‖ in the L2 operator norm.

Proof without integrals: the interpolant φ(s) = exp (s • C) · exp ((t−s) • A) has derivative exp (s • C) · (C − A) · exp ((t−s) • A), of norm at most ‖C − A‖ since both exponentials are unitary; the mean-value inequality on [0, t] finishes.

theorem Matrix.norm_exp_smul_neg_I_sub_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] (H H₀ : Matrix m m ℂ) (hH : H.IsHermitian) (hH₀ : H₀.IsHermitian) (t : ℝ) : ‖NormedSpace.exp (t • -Complex.I • H) - NormedSpace.exp (t • -Complex.I • H₀)‖ ≤ |t| * ‖H - H₀‖

The Duhamel bound for Hamiltonians. For Hermitian H, H₀, the Schrödinger unitaries stay within |t| · ‖H − H₀‖ of one another:

‖exp (t • (−i H)) − exp (t • (−i H₀))‖ ≤ |t| · ‖H − H₀‖.