Section 4 and equation (28): subadditivity with product equality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.subadditivity

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

prove2quantum

For a strictly positive trace-one bipartite state $\rho_{12}$ , with actual marginal states $\rho_1,\rho_2$ ,

S(\rho_{12})\le S(\rho_1)+S(\rho_2),

and equality holds if and only if $\rho_{12}=\rho_1\otimes\rho_2$ . This characterizes saturation of subadditivity by product states.

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]

/-- Section 4, equation (28), PDF pp.11–12: subadditivity with product equality. -/
theorem subadditivity [Nonempty A] [Nonempty B] (rho : Mat (A × B)) (h : FaithfulDensity rho) :
    entropy rho ≤ entropy (traceRight rho) + entropy (traceLeft rho) ∧
      (entropy rho = entropy (traceRight rho) + entropy (traceLeft rho) ↔
        rho = Matrix.kronecker (traceRight rho) (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, Section 4 and equation (28): subadditivity with product equality

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 definite complex matrix $\rho$ of trace $1$ on $A\times B$ , put $\rho_A=\operatorname{Tr}_B\rho$ and $\rho_B=\operatorname{Tr}_A\rho$ . Then

S(\rho)\le S(\rho_A)+S(\rho_B), \qquad S(\rho)=S(\rho_A)+S(\rho_B) \ \Longleftrightarrow\ \rho=\rho_A\otimes\rho_B.

Here partial traces sum over discarded indices, the tensor product has entries $(\rho_A)_{a,a'}(\rho_B)_{b,b'}$ , and $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ , where $f(x)=x\log x$ is applied by continuous functional calculus using natural logarithms. Singleton registers are allowed; positive definiteness is required of $\rho$ .

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