Equation (21): entropy triangle inequality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.entropyTriangle

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

prove2quantum

For any normalized positive semidefinite bipartite state $\rho_{12}$ , let $\rho_1,\rho_2$ be its partial traces. Then

|S(\rho_1)-S(\rho_2)|\le S(\rho_{12})\le S(\rho_1)+S(\rho_2).

Pure and singular states are included. This is the full two-sided entropy triangle inequality.

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]

/-- Equation (21), PDF p.9: both sides of the entropy triangle inequality. -/
theorem entropyTriangle [Nonempty A] [Nonempty B] (rho : Mat (A × B)) (h : IsDensityMatrix rho) :
    |entropy (traceRight rho) - entropy (traceLeft rho)| ≤ entropy rho ∧
      entropy rho ≤ entropy (traceRight rho) + entropy (traceLeft rho) := 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. 9, Equation (21): entropy triangle inequality

Read-back

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

For finite nonempty index types $A,B$ with decidable equality and every positive semidefinite complex matrix $\rho$ of trace $1$ on $A\times B$ , let $\rho_A=\operatorname{Tr}_B\rho$ and $\rho_B=\operatorname{Tr}_A\rho$ , where partial traces sum over the discarded index. Then

|S(\rho_A)-S(\rho_B)|\le S(\rho) \quad\text{and}\quad S(\rho)\le S(\rho_A)+S(\rho_B).

Here $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , where $f(x)=x\log x$ is applied by continuous functional calculus using natural logarithms and $\log0=0$ . The statement includes singular density matrices and singleton registers.

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