Theorem 7: joint convexity with equality

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.jointConvexity

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

prove2quantum

Let $\lambda_k>0$ be finitely many weights summing to one, and let $\rho_k,\gamma_k>0$ be positive definite matrices of a common size. Define $\rho=\sum_k\lambda_k\rho_k$ and $\gamma=\sum_k\lambda_k\gamma_k$ . Then

H(\rho,\gamma)\le\sum_k\lambda_kH(\rho_k,\gamma_k),

with equality if and only if $\log\rho-\log\gamma=\log\rho_k-\log\gamma_k$ for every $k$ . No trace-one or equal-trace hypothesis is imposed. This is the full cone version of joint convexity and its equality criterion.

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 7, PDF p.14: joint convexity and equality for positive weights and
positive definite pairs. Neither equal trace nor trace one is assumed. -/
theorem jointConvexity [Nonempty A] [Nonempty J] (w : J → ℝ) (hw : ∀ j, 0 < w j) (hs : ∑ j, w j = 1)
    (rho gamma : J → Mat A) (hr : ∀ j, (rho j).PosDef) (hg : ∀ j, (gamma j).PosDef) :
    (relativeEntropy (average w rho) (average w gamma)).toReal ≤ ∑ j, w j * (relativeEntropy (rho j) (gamma j)).toReal ∧
      ((relativeEntropy (average w rho) (average w gamma)).toReal =
        ∑ j, w j * (relativeEntropy (rho j) (gamma j)).toReal ↔
        ∀ j, logMatrix (average w rho) - logMatrix (average w gamma) =
          logMatrix (rho j) - logMatrix (gamma 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. 14, Theorem 7: joint convexity with equality

Read-back

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

For finite nonempty index types $A,J$ with decidable equality, let $w_j$ be strictly positive real numbers with $\sum_jw_j=1$ , and let $\rho_j,\gamma_j$ , $j\in J$ , be positive definite complex matrices on $A$ . Their traces are unrestricted. Define $\bar\rho=\sum_jw_j\rho_j$ , $\bar\gamma=\sum_jw_j\gamma_j$ , and, for positive definite matrices, $D(X\|Y)=\operatorname{Re}\operatorname{tr}(f(X)-X\log Y)$ , where $f(x)=x\log x$ and matrix functions use continuous functional calculus with natural logarithms; this equals the real conversion of the extended relative entropy appearing in the declaration. Then

D(\bar\rho\|\bar\gamma)\le\sum_jw_jD(\rho_j\|\gamma_j),

and equality holds if and only if, for every $j\in J$ ,

\log\bar\rho-\log\bar\gamma=\log\rho_j-\log\gamma_j.

Both index types may be singletons, and every weight is required to be nonzero.

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