The Lie–Trotter product formula in a Banach algebra

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

Glossary: https://glossary.constraintsurfacedynamics.com/lie-trotter-formula/ Plain-language, CSD-role and formal statements of the Lie-Trotter product formula, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

For arbitrary elements A, B of a complete normed algebra over ℝ with ‖1‖ = 1,

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

This de-skews the staged matrix trotter_skew (Mathlib/Analysis/Matrix/TrotterProduct.lean): skewness entered that proof exactly twice, and both uses generalize —

• ‖exp Y‖ = 1 in the one-step defect becomes ‖exp Y‖ ≤ e^{‖Y‖} (norm_exp_le_exp_norm), absorbed by the same final constant since the original calc already relaxes every factor to e^{‖X‖+‖Y‖};
• the norm-one telescoping becomes ‖Sⁿ − Tⁿ‖ ≤ n·Cⁿ·‖S − T‖ for ‖S‖, ‖T‖ ≤ C with 1 ≤ C (norm_pow_sub_pow_le_of_norm_le), and at step n the factors satisfy C = e^{s/n}, so Cⁿ = e^s stays bounded.

The chain:

• norm_exp_le_exp_norm — ‖exp X‖ ≤ e^{‖X‖} (termwise domination);
• norm_exp_sub_one_sub_le' — the second-order remainder ‖exp X − 1 − X‖ ≤ ‖X‖²·e^{‖X‖}, verbatim port of the matrix proof;
• norm_exp_mul_exp_sub_exp_add_le' — the one-step defect, hypothesis-free: ‖exp X · exp Y − exp (X+Y)‖ ≤ (‖X‖+‖Y‖)²(3+‖X‖+‖Y‖)e^{‖X‖+‖Y‖};
• norm_pow_sub_pow_le_of_norm_le — the growth-controlled telescoping;
• ★★ trotter_product — the product formula, with the explicit rate ‖(exp(A/n)exp(B/n))ⁿ − exp(A+B)‖ ≤ n⁻¹·s²(3+s)e^{2s}, s = ‖A‖+‖B‖.

Consumed by LF6/LindbladPositivity.lean in the endomorphism algebra of matrix space, where the two factors are the (positivity-preserving) drift and jump flows of a GKSL generator.

Provenance

Staged as upstream Mathlib material.

theorem NormedSpace.norm_exp_le_exp_norm {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (X : 𝔸) : ‖exp X‖ ≤ Real.exp ‖X‖

The exponential norm bound: ‖exp X‖ ≤ e^{‖X‖} (termwise domination of the exponential series).

theorem NormedSpace.norm_exp_sub_one_sub_le' {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (X : 𝔸) : ‖exp X - 1 - X‖ ≤ ‖X‖ ^ 2 * Real.exp ‖X‖

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

theorem NormedSpace.norm_exp_mul_exp_sub_exp_add_le' {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (X Y : 𝔸) : ‖exp X * exp Y - exp (X + Y)‖ ≤ (‖X‖ + ‖Y‖) ^ 2 * (3 + (‖X‖ + ‖Y‖)) * Real.exp (‖X‖ + ‖Y‖)

The one-step defect, hypothesis-free: for any X, Y, ‖exp X · exp Y − exp (X+Y)‖ ≤ (‖X‖+‖Y‖)²·(3+‖X‖+‖Y‖)·e^{‖X‖+‖Y‖} — the same constant as the skew case, since the skew proof already relaxed every exponential factor to e^{‖X‖+‖Y‖}.

theorem NormedSpace.norm_pow_sub_pow_le_of_norm_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormOneClass 𝔸] {S T : 𝔸} {C : ℝ} (hC : 1 ≤ C) (hS : ‖S‖ ≤ C) (hT : ‖T‖ ≤ C) (n : ℕ) : ‖S ^ n - T ^ n‖ ≤ ↑n * C ^ n * ‖S - T‖

Growth-controlled telescoping: for ‖S‖, ‖T‖ ≤ C with 1 ≤ C, ‖Sⁿ − Tⁿ‖ ≤ n · Cⁿ · ‖S − T‖.

theorem NormedSpace.exp_pow_eq_exp_nsmul {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (n : ℕ) : exp x ^ n = exp (n • x)

exp x ^ n = exp (n • x), by induction from exp_add_of_commute (the exp_nsmul route needs a ℚ-algebra instance a general real Banach algebra does not carry).

theorem NormedSpace.trotter_product {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (A B : 𝔸) : Filter.Tendsto (fun (n : ℕ) => (exp ((↑n)⁻¹ • A) * exp ((↑n)⁻¹ • B)) ^ n) Filter.atTop (nhds (exp (A + B)))

★★ The Lie–Trotter product formula in a Banach algebra: for any A, B, (exp (A/n) · exp (B/n))ⁿ → exp (A + B), at the explicit rate n⁻¹ · s²(3+s)e^{2s} with s = ‖A‖ + ‖B‖. The one-step defect is O(1/n²), the telescoping costs n · (e^{s/n})ⁿ = n·e^s, and the total O(1/n) squeezes to zero.