Theorem 3: Klein inequality with equality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.klein

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

prove2quantum

Let $A,B$ be positive definite matrices of the same size. With $H(A,B)=\operatorname{Tr}A(\log A-\log B)$ ,

H(A,B)\ge\operatorname{Tr}(A-B),\qquad H(A,B)=\operatorname{Tr}(A-B)\iff A=B.

No equality of traces or normalization is required. Klein’s inequality supplies the equality criterion used in the entropy inequalities.

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 3, PDF p.8: Klein's inequality and equality, with no trace normalization. -/
theorem klein [Nonempty A] (X Y : Mat A) (hX : X.PosDef) (hY : Y.PosDef) :
    (X - Y).trace.re ≤ (relativeEntropy X Y).toReal ∧
      ((relativeEntropy X Y).toReal = (X - Y).trace.re ↔ X = Y) := 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 3: Klein inequality with 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 positive definite complex matrices $X,Y$ indexed by $A$ , the theorem asserts

\operatorname{Re}\operatorname{tr}(X-Y) \le \operatorname{Re}\operatorname{tr}\!\left(f(X)-X\log Y\right), \qquad f(x)=x\ln x,

and equality holds if and only if $X=Y$ . The functions $f$ and the natural logarithm are applied through continuous functional calculus. The right-hand side is the real conversion of the defined extended relative entropy: that definition uses this trace expression when $\ker Y\subseteq\ker X$ , and $+\infty$ otherwise; positive definiteness here ensures the support condition. Neither matrix is required to have trace one, and singleton index types are included.

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