Section 5.3: convexity of negative conditional entropy

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.negativeConditionalEntropyConvex

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

prove2quantum

Let $\lambda_k\ge0$ sum to one and let $\rho^{(k)}_{12}$ be finite normalized PSD states, with $\rho_{12}=\sum_k\lambda_k\rho^{(k)}_{12}$ . Then

S(\rho_1)-S(\rho_{12})\le\sum_k\lambda_k\bigl[S(\rho^{(k)}_1)-S(\rho^{(k)}_{12})\bigr].

The marginal index is $1$ , and all marginal states are partial traces. This is convexity of negative conditional entropy of system $2$ conditioned on $1$ , including singular 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 5.3, PDF pp.14–15: convexity of S(rho1)-S(rho12); the marginal is 1.
PSD block states are allowed. -/
theorem negativeConditionalEntropyConvex [Nonempty A] [Nonempty B] [Nonempty J] (w : J → ℝ) (hw : IsLaw w)
    (rho : J → Mat (A × B)) (hr : ∀ j, IsDensityMatrix (rho j)) :
    entropy (traceRight (average w rho)) - entropy (average w rho) ≤
      ∑ j, w j * (entropy (traceRight (rho j)) - entropy (rho j)) := 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. 15, Section 5.3: convexity of negative conditional entropy

Read-back

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

For finite nonempty index types $A,B,J$ , each with decidable equality, let $w:J\to\mathbb R$ satisfy $w_j\ge0$ for every $j$ and $\sum_jw_j=1$ , and let each $\rho_j$ be a positive semidefinite complex matrix of trace $1$ on $A\times B$ . Writing $\bar\rho=\sum_jw_j\rho_j$ , the assertion is

S(\operatorname{Tr}_B\bar\rho)-S(\bar\rho) \le \sum_jw_j\bigl(S(\operatorname{Tr}_B\rho_j)-S(\rho_j)\bigr).

Here $(\operatorname{Tr}_BX)_{a,a'}=\sum_bX_{(a,b),(a',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 and $\log0=0$ . Zero weights, singular density matrices, 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