The exponential is the unique solution of U' = X U, U 0 = 1; the closed form for X² = P

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #183.

In a complete normed algebra over ℝ or ℂ, a differentiable U with U 0 = 1 and U' a = X * U a for all a is a ↦ exp (a • X): the function a ↦ exp (−a • X) * U a has zero derivative, so it is constant, and equals 1 at 0. This replaces series manipulations by an ODE argument whenever a candidate closed form is at hand.

The application: if X * X = P and X * P = X (so X is an "involution on its own range", e.g. a symmetric hop |10⟩⟨01| + |01⟩⟨10| with P the projector on the two configurations it exchanges), then exp (a • X) = 1 + (cosh a − 1) • P + sinh a • X for every a : ℂ.

• exp_smul_mul_exp_neg_smul — exp (a • X) * exp (−a • X) = 1;
• ★★ exp_smul_eq_of_hasDerivAt — uniqueness: U 0 = 1 and U' = X U force U a = exp (a • X);
• ★★ exp_smul_eq_cosh_sinh — the closed form for X² = P, X P = X.

Honest scope

• The uniqueness statement is for the left equation U' = X U; the right equation U' = U X is the same proof with the factors swapped and is not duplicated.
• The closed form is stated over ℂ, where cosh and sinh live; the purely imaginary case a = −iθ gives cos θ and −i sin θ through Complex.cosh_mul_I, Complex.sinh_mul_I.

References: Mathlib/Analysis/SpecialFunctions/Exponential.lean (hasDerivAt_exp_smul_const), Mathlib/Analysis/Calculus/MeanValue.lean (is_const_of_deriv_eq_zero); specs/BACKLOG.md #183.

theorem exp_smul_mul_exp_neg_smul {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (X : 𝔸) (a : 𝕂) : NormedSpace.exp (a • X) * NormedSpace.exp (-a • X) = 1

theorem exp_smul_eq_of_hasDerivAt {𝕂 : Type u_1} {𝔸 : Type u_2} [RCLike 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {U : 𝕂 → 𝔸} (X : 𝔸) (h0 : U 0 = 1) (hU : ∀ (a : 𝕂), HasDerivAt U (X * U a) a) (a : 𝕂) : U a = NormedSpace.exp (a • X)

★★ Uniqueness of the exponential as an ODE solution: if U 0 = 1 and U' a = X * U a for every a, then U a = exp (a • X).

theorem exp_smul_eq_cosh_sinh {𝔸 : Type u_1} [NormedRing 𝔸] [NormedAlgebra ℂ 𝔸] [CompleteSpace 𝔸] {X P : 𝔸} (hXX : X * X = P) (hXP : X * P = X) (a : ℂ) : NormedSpace.exp (a • X) = 1 + (Complex.cosh a - 1) • P + Complex.sinh a • X

★★ The closed form for X² = P, X P = X: exp (a • X) = 1 + (cosh a − 1) • P + sinh a • X.