The Exercise

A system evolves under a Hamiltonian $H = A + B$ that is the sum of two Hermitian terms, each of which is easy to evolve under alone. When $A$ and $B$ do not commute, the evolution $e^{-iHt}$ for a time $t$ is in general not $e^{-iAt} e^{-iBt}$ . The Trotter formula recovers it from the two pieces: cut $t$ into $n$ steps of length $t/n$ , in each step evolve under $A$ for $t/n$ and then under $B$ for $t/n$ , and the product of the $n$ steps tends to $e^{-iHt}$ as $n$ grows, for every real $t$ .

A Real Banach Algebra

The library states the Lie product formula, for any two elements of a real Banach algebra. A real Banach algebra $\mathcal{A}$ is an algebra over the real numbers with a norm in which it is complete and which satisfies $\|xy\| \le \|x\| \, \|y\|$ . The exponential of an element $x$ of $\mathcal{A}$ is the sum of the power series $\exp(x) = \sum_{k=0}^{\infty} \frac{x^{k}}{k!},$ (1) which converges in norm for every $x$ . On the operators of a finite-dimensional system’s state space, with the operator norm, this is a real Banach algebra, and there (1) is the matrix exponential.

The Claim

Theorem 1. Let $\mathcal{A}$ be a real Banach algebra, and let $x$ and $y$ be any two elements of $\mathcal{A}$ , commuting or not. Then, in the norm of $\mathcal{A}$ , $\lim_{n \to \infty} \Bigl( \exp\bigl(\tfrac{x}{n}\bigr) \exp\bigl(\tfrac{y}{n}\bigr) \Bigr)^{n} = \exp(x + y).$ (2)^✦

With $x = -iAt$ and $y = -iBt$ in the algebra of operators on the state space, this is the Trotter formula of the exercise.

What Is Checked

About $\mathcal{A}$ , $x$ , and $y$ , the library proves the limit (2).^✦