Equation (29): Araki–Lieb overlapping-subsystem entropy bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.overlappingEntropy

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

prove2quantum

Let $\rho_{123}>0$ have trace one on three finite systems, with reduced states $\rho_{12}$ and $\rho_{23}$ . Then

S(\rho_{123})\le S(\rho_{12})+S(\rho_{23}).

This is the overlapping-subsystem inequality (29); the trace-one constraint is essential to the source’s statement.

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 (29), PDF p.12: the overlapping-subsystem bound, with trace one. -/
theorem overlappingEntropy [Nonempty A] [Nonempty B] [Nonempty C] (rho : Mat (A × (B × C))) (h : FaithfulDensity rho) :
    entropy rho ≤ entropy (marginalAB 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. 12, Equation (29): Araki–Lieb overlapping-subsystem entropy bound

Read-back

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

For finite nonempty index types $A,B,C$ , each with decidable equality, and every positive definite complex matrix $\rho$ of trace $1$ on $A\times(B\times C)$ , one has

S(\rho)\le S(\rho_{AB})+S(\rho_{BC}),

where $(\rho_{AB})_{(a,b),(a',b')}=\sum_c\rho_{(a,(b,c)),(a',(b',c))}$ , $(\rho_{BC})_{(b,c),(b',c')}=\sum_a\rho_{(a,(b,c)),(a,(b',c'))}$ , and $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , with $f(x)=x\log x$ applied by continuous functional calculus using natural logarithms. Each register may have cardinality $1$ .

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