The commutator-scaling error bound

For A, B in a complete normed algebra over ℝ with ‖1‖ = 1 and every n ≥ 1,

‖(exp (A/n) · exp (B/n))ⁿ − exp (A + B)‖ ≤ ‖AB − BA‖ / (2n) · e^{‖A‖ + ‖B‖}.

The bound vanishes when A and B commute. The constant 1/2 is sharp (not proved here): for small A, B the product is exp (A + B + [A, B]/(2n) + O(1/n²)). The exponential factor is not sharp. Adapted for Lean Pool's module paths and imports from the Apache-2.0 upstream development.

The chain:

• norm_exp_smul_mul_sub_le: ‖exp (tA) B − B exp (tA)‖ ≤ t ‖AB − BA‖ e^{t‖A‖} for t ≥ 0, from the derivative of σ ↦ exp (σA) B exp ((t − σ)A), which is exp (σA) (AB − BA) exp ((t − σ)A);
• norm_exp_mul_exp_sub_exp_add_le_commutator: the one-step bound ‖exp A exp B − exp (A + B)‖ ≤ ‖AB − BA‖/2 · e^{‖A‖+‖B‖}. The function H τ = exp ((1 − τ)(A + B)) exp (τA) exp (τB) runs from exp (A + B) to exp A exp B, and its derivative is exp ((1 − τ)(A + B)) (exp (τA) B − B exp (τA)) exp (τB), of norm at most τ ‖AB − BA‖ e^{‖A‖+‖B‖}. The mean value inequality against τ²/2 gives the factor 1/2;
• norm_pow_succ_sub_pow_succ_le: telescoping, ‖Sⁿ⁺¹ − Tⁿ⁺¹‖ ≤ (n + 1) Cⁿ ‖S − T‖ when ‖S‖, ‖T‖ ≤ C;
• norm_trotter_sub_le_commutator: the bound above, with n steps of size 1/n.

theorem LieTrotter.norm_exp_smul_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (X : 𝔸) {t : ℝ} (ht : 0 ≤ t) : ‖NormedSpace.exp (t • X)‖ ≤ Real.exp (t * ‖X‖)

‖exp (t • X)‖ ≤ e^{t ‖X‖} for t ≥ 0.

theorem LieTrotter.hasDerivAt_exp_const_sub_smul {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (X : 𝔸) (c σ : ℝ) : HasDerivAt (fun (σ : ℝ) => NormedSpace.exp ((c - σ) • X)) (-(X * NormedSpace.exp ((c - σ) • X))) σ

The derivative of σ ↦ exp ((c − σ) • X) is -(X * exp ((c − σ) • X)).

theorem LieTrotter.hasDerivAt_exp_const_sub_smul' {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] (X : 𝔸) (c σ : ℝ) : HasDerivAt (fun (σ : ℝ) => NormedSpace.exp ((c - σ) • X)) (-(NormedSpace.exp ((c - σ) • X) * X)) σ

The derivative of σ ↦ exp ((c − σ) • X), with X on the right.

theorem LieTrotter.norm_exp_smul_mul_sub_le {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (A B : 𝔸) {t : ℝ} (ht : 0 ≤ t) : ‖NormedSpace.exp (t • A) * B - B * NormedSpace.exp (t • A)‖ ≤ t * ‖A * B - B * A‖ * Real.exp (t * ‖A‖)

The commutator with an exponential. For t ≥ 0, ‖exp (t • A) * B − B * exp (t • A)‖ ≤ t ‖AB − BA‖ e^{t ‖A‖}.

theorem LieTrotter.norm_exp_mul_exp_sub_exp_add_le_commutator {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] (A B : 𝔸) : ‖NormedSpace.exp A * NormedSpace.exp B - NormedSpace.exp (A + B)‖ ≤ ‖A * B - B * A‖ / 2 * Real.exp (‖A‖ + ‖B‖)

The one-step bound with the commutator. ‖exp A * exp B − exp (A + B)‖ ≤ ‖AB − BA‖ / 2 · e^{‖A‖ + ‖B‖}.

theorem LieTrotter.norm_trotter_sub_le_commutator {𝔸 : 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)‖ ≤ ‖A * B - B * A‖ / (2 * ↑n) * Real.exp (‖A‖ + ‖B‖)

The Lie–Trotter product formula with commutator scaling. For n ≥ 1, ‖(exp (A/n) · exp (B/n))ⁿ − exp (A + B)‖ ≤ ‖AB − BA‖ / (2n) · e^{‖A‖ + ‖B‖}.

theorem LieTrotter.trotter_eq_of_commute {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℝ 𝔸] [CompleteSpace 𝔸] [NormOneClass 𝔸] {A B : 𝔸} (h : Commute A B) (n : ℕ) (hn : 1 ≤ n) : (NormedSpace.exp ((↑n)⁻¹ • A) * NormedSpace.exp ((↑n)⁻¹ • B)) ^ n = NormedSpace.exp (A + B)

When A and B commute, the product formula is exact at every step: the error bound vanishes.