The Lie–Trotter product formula in a Banach algebra

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

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

with the explicit rate ‖(exp (A/n) · exp (B/n))ⁿ − exp (A + B)‖ ≤ n⁻¹ · s²(3 + s)e^{2s} for every n ≥ 1, where s = ‖A‖ + ‖B‖.

The chain:

• norm_exp_le_exp_norm: ‖exp X‖ ≤ e^{‖X‖}, by termwise domination of the series;
• norm_exp_sub_one_sub_le: the second-order remainder ‖exp X − 1 − X‖ ≤ ‖X‖² e^{‖X‖};
• 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‖};
• norm_pow_sub_pow_le_of_norm_le: telescoping, ‖Sⁿ − Tⁿ‖ ≤ n Cⁿ ‖S − T‖ when ‖S‖, ‖T‖ ≤ C and 1 ≤ C;
• norm_trotter_sub_le: the explicit rate. At step n the one-step defect is O(1/n²) and the telescoping costs n (e^{s/n})ⁿ = n e^s, so the total is O(1/n);
• trotter_product: the product formula.

This is the general form of the Lie product formula (after Sophus Lie, for matrices; H. F. Trotter, 1959, for operator semigroups), in the bounded case: any real Banach algebra.

The file is extracted from csd-lean4 (CsdLean4/Mathlib/Analysis/NormedSpace/TrotterGeneral.lean, https://github.com/zblore/csd-lean4), where it was added on 20 Aug 2026. Adapted for Lean Pool: the series estimates use HasSum.norm_le_of_bounded directly, avoiding repeated summability and tsum conversions and removing heartbeat overrides.

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

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

theorem LieTrotter.norm_exp_sub_one_sub_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (X : 𝔸) : ‖NormedSpace.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 LieTrotter.norm_exp_mul_exp_sub_exp_add_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (X 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 any X, Y, with no commutativity assumption: ‖exp X · exp Y − exp (X+Y)‖ ≤ (‖X‖+‖Y‖)²·(3+‖X‖+‖Y‖)·e^{‖X‖+‖Y‖}.

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

Telescoping: for ‖S‖, ‖T‖ ≤ C, ‖Sⁿ⁺¹ − Tⁿ⁺¹‖ ≤ (n + 1) Cⁿ ‖S − T‖.

theorem LieTrotter.norm_pow_sub_pow_le_of_norm_le {𝔸 : Type u_1} [NormedRing 𝔸] {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 LieTrotter.exp_pow_eq_exp_nsmul {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (n : ℕ) : NormedSpace.exp x ^ n = NormedSpace.exp (n • x)

exp x ^ n = exp (n • x), by induction from exp_add_of_commute. (Mathlib's exp_nsmul needs a ℚ-algebra instance, which instance search does not find for a general real Banach algebra; it could be supplied by restricting scalars from ℝ to ℚ.)

theorem LieTrotter.norm_trotter_sub_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (A B : 𝔸) (n : ℕ) (hn : 1 ≤ n) : ‖(NormedSpace.exp ((↑n)⁻¹ • A) * NormedSpace.exp ((↑n)⁻¹ • B)) ^ n - NormedSpace.exp (A + B)‖ ≤ (↑n)⁻¹ * ((‖A‖ + ‖B‖) ^ 2 * (3 + (‖A‖ + ‖B‖)) * Real.exp (2 * (‖A‖ + ‖B‖)))

The explicit rate. For n ≥ 1, ‖(exp (A/n) · exp (B/n))ⁿ − exp (A + B)‖ ≤ n⁻¹ · s²(3 + s)e^{2s} with s = ‖A‖ + ‖B‖. The one-step defect is O(1/n²), and the telescoping costs n · (e^{s/n})ⁿ = n e^s.

theorem LieTrotter.trotter_product {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (A 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 in a Banach algebra: for any A, B, (exp (A/n) · exp (B/n))ⁿ → exp (A + B).