Lie-Trotter product formula

In plain terms

For ordinary numbers, the exponential of a sum is the product of the exponentials. For operations that don't commute, meaning the result depends on the order in which they're applied, this fails, and in quantum mechanics, where evolution over a stretch of time is the exponential of an energy generator, the interesting pieces of the generator never commute.

The Lie-Trotter formula is the repair. Alternate many tiny steps of each piece, and in the limit of ever smaller steps you recover the exponential of the sum exactly. Physicists use this daily, as it's the licence behind every quantum simulation, in which a complicated evolution is approximated by a sequence of simple ones.

The corpus needed the formula in a form its libraries didn't have, for operators acting on the space of matrices, as the generator of an open-system evolution does, with a quantitative error, and without special structural assumptions on the pieces. So it was proved from scratch at textbook generality, for any complete normed algebra, a setting in which elements can be added, multiplied and measured for size and in which limits exist, with an explicit rate of convergence. The defect of a single step is controlled by an estimate on the tail of a series, and the defects are added up without growth.

In CSD

The formula is the assembly step in the proof that the Lindblad flow is completely positive. The drift part and the jump part of the generator separately generate evolutions that preserve positivity, and the product formula is what lets their alternation converge to the full evolution, so positivity passes to the limit.

It's staged as a candidate for contribution to Mathlib, free of anything CSD- specific by construction, the kind of infrastructure the formalisation deliberately leaves better than it found it.

Mathematically

The theorem NormedSpace.trotter_product states that in a complete normed real algebra with unit norm one, the n-fold alternating product of exp(A/n) and exp(B/n) converges to exp(A+B), with a one-step defect of order one over n squared, telescoped to an overall rate with the explicit constant s^2 (3 + s) e^(2s) over n for s the sum of the norms.

The earlier staged version required skew-adjointness, and the de-skewed form replaces the two places skewness entered by norm bounds the final constant absorbs.

The name

Hale Trotter (1931-2022) was a Canadian-American mathematician at Princeton, and the 1959 product formula came out of his thesis work on semigroups of operators. The finite-dimensional antecedent is Sophus Lie's, from the nineteenth-century theory of continuous groups, which is why the formula carries both names, and Masuo Suzuki's later higher-order refinements are why simulation people say Trotter-Suzuki.

Related entries

• Lindblad equationThe master equation of open quantum systems is formalised end to end, as the evolution generated by every Lindblad generator is proved to be completely positive, with the bystander-system argument carried out rather than gestured at.
• Stone's theoremAsk only that time evolution never jumps, and differentiability, a generator and the Hamiltonian all follow for free.
• Schrodinger equationIn CSD the Schrodinger equation isn't postulated, as it's what any continuous motion that preserves the measurable relations between quantum states is forced to look like.
• What exactly is machine-checked in CSD?Every theorem in the CSD corpus is verified by a proof assistant from zero imported axioms, and the list of what such checking can't certify is published alongside it.
• Quantum channelThe most general thing that can happen to a quantum state is captured in CSD as a concrete structure, a family of operators with one completeness law, and every certificate of its physicality is proved rather than assumed.