The Lie–Trotter product formula for skew-Hermitian matrices

Category: 1-Mathlib (CSD-free, staged for upstream).

For skew-Hermitian A, B (so all exponentials are unitary),

(exp (A/n) · exp (B/n))ⁿ → exp (A + B)

in the L2 operator norm. The chain:

• norm_exp_sub_one_sub_le — the quantitative second-order remainder ‖exp X − 1 − X‖ ≤ ‖X‖² · e^{‖X‖} (tail of the exponential series, termwise dominated);
• norm_exp_mul_exp_sub_exp_add_le — the one-step defect ‖exp X · exp Y − exp (X+Y)‖ ≤ (‖X‖+‖Y‖)²(3+‖X‖+‖Y‖)e^{‖X‖+‖Y‖} for skew X, Y (the algebraic four-term split, with the unitary factors at norm one);
• norm_pow_sub_pow_le_of_unitary — the growth-free telescoping ‖Sⁿ − Tⁿ‖ ≤ n·‖S − T‖ for unitaries;
• ★★ trotter_skew — the product formula: the one-step defect is O(1/n²), the telescoping multiplies by n, and the total O(1/n) squeezes to zero.

Consumed by the CSD chain as CV-12 (specs/eft-stage4-plan.md): the interacting drive for an arbitrary Hermitian V becomes a limit of constructible steps. No Trotter statement exists in Mathlib at the pin (checked 2026-08-09); the skew-Hermitian case is the natural first upstream cut, since unitarity removes all growth factors.

Provenance

Staged as upstream Mathlib material; L2 operator norm scope, as DuhamelBound.lean.

theorem Matrix.exp_mem_unitaryGroup_of_skew {m : Type u_1} [Fintype m] [DecidableEq m] {X : Matrix m m ℂ} (hX : X.conjTranspose = -X) : NormedSpace.exp X ∈ unitaryGroup m ℂ

Skew-Hermitian exponentials are unitary (membership form).

theorem Matrix.l2_opNorm_exp_skew {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {X : Matrix m m ℂ} (hX : X.conjTranspose = -X) : ‖NormedSpace.exp X‖ = 1

Skew-Hermitian exponentials have unit norm.

theorem Matrix.norm_exp_sub_one_sub_le {m : Type u_1} [Fintype m] [DecidableEq m] (X : Matrix m m ℂ) : ‖NormedSpace.exp X - 1 - X‖ ≤ ‖X‖ ^ 2 * Real.exp ‖X‖

The quantitative second-order remainder: ‖exp X − 1 − X‖ ≤ ‖X‖² · e^{‖X‖}.

theorem Matrix.norm_exp_mul_exp_sub_exp_add_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {X Y : Matrix m m ℂ} (hY : Y.conjTranspose = -Y) : ‖NormedSpace.exp X * NormedSpace.exp Y - NormedSpace.exp (X + Y)‖ ≤ (‖X‖ + ‖Y‖) ^ 2 * (3 + (‖X‖ + ‖Y‖)) * Real.exp (‖X‖ + ‖Y‖)

The one-step defect for skew-Hermitian X, Y: ‖exp X · exp Y − exp (X+Y)‖ ≤ (‖X‖+‖Y‖)²·(3+‖X‖+‖Y‖)·e^{‖X‖+‖Y‖}.

theorem Matrix.norm_pow_sub_pow_le_of_unitary {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S T : Matrix m m ℂ} (hS : S ∈ unitaryGroup m ℂ) (hT : T ∈ unitaryGroup m ℂ) (n : ℕ) : ‖S ^ n - T ^ n‖ ≤ ↑n * ‖S - T‖

Growth-free telescoping: for unitaries, ‖Sⁿ − Tⁿ‖ ≤ n · ‖S − T‖.

theorem Matrix.trotter_skew {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {A B : Matrix m m ℂ} (hA : A.conjTranspose = -A) (hB : B.conjTranspose = -B) : Filter.Tendsto (fun (n : ℕ) => (NormedSpace.exp ((↑n)⁻¹ • A) * NormedSpace.exp ((↑n)⁻¹ • B)) ^ n) Filter.atTop (nhds (NormedSpace.exp (A + B)))

★★ The Lie–Trotter product formula, skew-Hermitian case: (exp (A/n) · exp (B/n))ⁿ → exp (A + B). The one-step defect is O(1/n²), the unitary telescoping multiplies by n, and the total O(1/n) squeezes to zero.