Theorem 4: Golden–Thompson–Symanzik and equality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.goldenThompson

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For any two self-adjoint matrices $A,B$ on the same finite system,

\operatorname{Tr}e^{A+B}\le\operatorname{Tr}(e^Ae^B),

and equality holds if and only if $AB=BA$ . This gives both the Golden–Thompson–Symanzik trace bound and its exact commutation criterion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P56 (entropy holevo IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Theorem 4, PDF p.8: Golden–Thompson–Symanzik with equality iff commutation. -/
theorem goldenThompson [Nonempty A] (X Y : Mat A) (hX : X.IsHermitian) (hY : Y.IsHermitian) :
    (NormedSpace.exp (X + Y)).trace.re ≤ (NormedSpace.exp X * NormedSpace.exp Y).trace.re ∧
      ((NormedSpace.exp (X + Y)).trace.re = (NormedSpace.exp X * NormedSpace.exp Y).trace.re ↔
        X * Y = Y * X) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 8, Theorem 4: Golden–Thompson–Symanzik and equality

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every nonempty finite index type $A$ with decidable equality and every pair of Hermitian complex matrices $X,Y$ indexed by $A$ , the theorem asserts

\operatorname{Re}\operatorname{tr}e^{X+Y} \le \operatorname{Re}\operatorname{tr}(e^Xe^Y),

and

\operatorname{Re}\operatorname{tr}e^{X+Y} = \operatorname{Re}\operatorname{tr}(e^Xe^Y) \quad\Longleftrightarrow\quad XY=YX.

The exponentials are matrix exponentials. No positivity or trace normalization is required, and the statement includes one-dimensional index types.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph