Sections 7.1–7.3: Holevo bound is attainable iff active states commute

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.holevoAttainment

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

prove2quantum

Fix a finite ensemble $\mathcal E=\{\pi_j,\rho_j\}$ of normalized PSD states with nonnegative weights summing to one. Its Holevo quantity is $\chi(\mathcal E)$ and $I(\mathcal E,\mathcal M)$ is the classical information extracted by a POVM. Then

\exists\,\mathcal M:\ I(\mathcal E,\mathcal M)=\chi(\mathcal E)\iff[\rho_j,\rho_k]=0\ \text{for all }\pi_j,\pi_k>0.

When the active states commute, a unitary simultaneous diagonalization gives a rank-one spectral projective measurement attaining equality. This is an existence and witness assertion, allowing singular states; it does not require every attaining POVM to be projective.

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]

/-- Sections 7.1–7.3, PDF pp.17–20: existence of an attaining POVM iff active
states commute, and a simultaneous spectral projective witness in that case. -/
theorem holevoAttainment [Nonempty A] [Nonempty J] (w : J → ℝ) (hw : IsLaw w)
    (rho : J → Mat A) (hr : ∀ j, IsDensityMatrix (rho j)) :
    let commuting := ∀ j k, 0 < w j → 0 < w k → rho j * rho k = rho k * rho j
    ((∃ m : ℕ, 0 < m ∧ ∃ E : Fin m → Mat A, IsPOVM E ∧
      (Real.log 2 * measurementInformation w rho E) = holevo w rho) ↔ commuting) ∧
    (commuting → ∃ U : Mat A, Uᴴ * U = 1 ∧ U * Uᴴ = 1 ∧
      (∀ j, 0 < w j → ∀ a b, a ≠ b → (Uᴴ * rho j * U) a b = 0) ∧
      IsPOVM (basisPVM U) ∧
      (∀ a b, basisPVM U a * basisPVM U b = if a = b then basisPVM U a else 0) ∧
      (Real.log 2 * measurementInformation w rho (basisPVM U)) = holevo w 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. 17, Sections 7.1–7.3: Holevo bound is attainable iff active states commute

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 as required for matrix operations, let $w_j\ge0$ , $\sum_jw_j=1$ , and let every $\rho_j$ be positive semidefinite with trace one. Define $\bar\rho=\sum_jw_j\rho_j$ , $S(X)=-\operatorname{Re}\operatorname{tr}[f(X)]$ with $f(x)=x\ln x$ applied by continuous functional calculus, and $\chi=S(\bar\rho)-\sum_jw_jS(\rho_j)$ . For a finite measurement $E$ , define $p_{b|j}=\operatorname{Re}\operatorname{tr}(E_b\rho_j)$ and

I(w,\rho,E)=H_2\!\left(\left(\sum_jw_jp_{b|j}\right)_b\right) -\sum_jw_jH_2((p_{b|j})_b),\qquad H_2(p)=-\sum_bp_b\log_2p_b.

Then there exist a natural number $m>0$ and positive semidefinite effects $E_0,\ldots,E_{m-1}$ summing to $I_A$ , with $(\ln2)I(w,\rho,E)=\chi$ , if and only if $\rho_j\rho_k=\rho_k\rho_j$ whenever $w_j>0$ and $w_k>0$ . Moreover, if this commutation condition holds, there exists a matrix $U$ on $A$ with $U^\dagger U=UU^\dagger=I_A$ such that every $U^\dagger\rho_jU$ with $w_j>0$ has zero off-diagonal entries; the matrices $P_a$ , defined by $(P_a)_{ij}=U_{ia}\overline{U_{ja}}$ , are positive semidefinite, sum to $I_A$ , satisfy $P_aP_b=P_a$ when $a=b$ and $P_aP_b=0$ otherwise, and obey $(\ln2)I(w,\rho,P)=\chi$ . Zero weights are permitted, and no commutation or diagonalization condition is imposed on their corresponding states; logarithmic expressions use value zero at zero.

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