Equations (47)–(50): Holevo measurement bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.holevoMeasurementBound

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

prove2quantum

Let $\mathcal E=\{\pi_j,\rho_j\}$ be any finite ensemble of normalized PSD states, with nonnegative weights summing to one and average $\bar\rho=\sum_j\pi_j\rho_j$ . For every finite POVM $\mathcal M=\{E_b\}$ , set $p_j(b)=\operatorname{Tr}(E_b\rho_j)$ and $p(b)=\operatorname{Tr}(E_b\bar\rho)$ . With Shannon entropy $H_{\rm Sh}$ in nats,

I(\mathcal E,\mathcal M):=H_{\rm Sh}(p)-\sum_j\pi_jH_{\rm Sh}(p_j)\le\chi(\mathcal E):=S(\bar\rho)-\sum_j\pi_jS(\rho_j)=\sum_{j:\pi_j>0}\pi_jH(\rho_j,\bar\rho).

Zero probabilities use the entropy convention $0\log0=0$ . This is the pointwise Holevo measurement bound, including singular ensembles.

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]

/-- Equations (47)–(50), PDF pp.17–18: the Holevo bound for every POVM, together
with its relative-entropy expression; only active labels enter that expression. -/
theorem holevoMeasurementBound [Nonempty A] [Nonempty J] [Nonempty O] (w : J → ℝ) (hw : IsLaw w)
    (rho : J → Mat A) (hr : ∀ j, IsDensityMatrix (rho j)) (E : O → Mat A) (hE : IsPOVM E) :
    (Real.log 2 * measurementInformation w rho E) ≤ holevo w rho ∧
      holevo w rho = ∑ j, if 0 < w j then w j * (relativeEntropy (rho j) (average w rho)).toReal else 0 := 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, Equations (47)–(50): Holevo measurement bound

Read-back

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

For finite nonempty index types $A,J,O$ , with decidable equality as required for the matrix definitions, let $w:J\to\mathbb R$ satisfy $w_j\ge0$ and $\sum_jw_j=1$ , let every $\rho_j$ be a positive semidefinite trace-one matrix on $A$ , and let $E_o$ be positive semidefinite matrices with $\sum_oE_o=I_A$ . Put $\bar\rho=\sum_jw_j\rho_j$ , $p_{o|j}=\operatorname{Re}\operatorname{tr}(E_o\rho_j)$ , $p_o=\sum_jw_jp_{o|j}$ , $H_2(p)=-\sum_op_o\log_2p_o$ , and $S(X)=-\operatorname{Re}\operatorname{tr}[f(X)]$ , where $f(x)=x\ln x$ is applied by continuous functional calculus. Then

(\ln2)\left[H_2((p_o)_o)-\sum_jw_jH_2((p_{o|j})_o)\right] \le S(\bar\rho)-\sum_jw_jS(\rho_j) =\sum_{\substack{j\in J\\w_j>0}}w_jD_{\mathbb R}(\rho_j\Vert\bar\rho).

Here $D(X\Vert Y)$ is $\operatorname{Re}\operatorname{tr}[f(X)-X\log Y]$ if $\ker Y\subseteq\ker X$ , and $+\infty$ otherwise, and $D_{\mathbb R}$ is its real conversion, sending $+\infty$ to zero. All logarithms use their total real definitions, including value zero at zero. Zero weights and zero measurement effects are allowed, and the displayed relative-entropy sum assigns zero to every term with $w_j=0$ .

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