Section 7.4: attainability of Hall bound and commutation consequence

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.hallAttainment

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

prove2quantum

Fix a faithful density matrix $\rho$ and a finite POVM $\{E_b\}$ , allowing zero or singular effects. Let $Q_b=\sqrt\rho E_b\sqrt\rho$ , and let $B_{\rm Hall}(\rho,\mathcal M)$ be Hall’s right side with null outcomes deleted. Then

\exists\,\mathcal E\text{ of average }\rho:\ I(\mathcal E,\mathcal M)=B_{\rm Hall}(\rho,\mathcal M)\iff[Q_b,Q_c]=0\quad\forall b,c.

Moreover, this commutation implies $[\rho,E_b]=0$ for every $b$ . The ensemble varies subject to its average; no channel-image constraint is imposed.

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 7.4, PDF p.21: existence of an attaining ensemble for fixed rho,E,
with the commutation consequence; the ensemble is varied subject to its average. -/
theorem hallAttainment [Nonempty A] [Nonempty O] (rho : Mat A) (hr : FaithfulDensity rho) (E : O → Mat A) (hE : IsPOVM E) :
    let commuting := ∀ b c, dualUnnormalized rho E b * dualUnnormalized rho E c =
      dualUnnormalized rho E c * dualUnnormalized rho E b
    ((∃ m : ℕ, 0 < m ∧ ∃ w : Fin m → ℝ, IsLaw w ∧
      ∃ sigma : Fin m → Mat A, (∀ j, IsDensityMatrix (sigma j)) ∧ average w sigma = rho ∧
        (Real.log 2 * measurementInformation w sigma E) = hallBound rho E) ↔ commuting) ∧
    (commuting → ∀ b, rho * E b = E b * 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. 21, Section 7.4: attainability of Hall bound and commutation consequence

Read-back

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

For finite nonempty index types $A,O$ , with decidable equality as required for matrix operations, let $\rho$ be positive definite with trace one, and let $E_b$ be positive semidefinite matrices summing to $I_A$ . Define $T_b=\rho^{1/2}E_b\rho^{1/2}$ , $p_b=\operatorname{Re}\operatorname{tr}(E_b\rho)$ , $\tau_b=p_b^{-1}T_b$ , and

H_{\mathrm{Hall}}(\rho,E) =S(\rho)-\sum_{\substack{b\in O\\p_b>0}}p_bS(\tau_b), \qquad S(X)=-\operatorname{Re}\operatorname{tr}[f(X)],\quad f(x)=x\ln x,

where square roots and $f$ use continuous functional calculus, scalar inversion sends zero to zero, and the real logarithm has value zero at zero. Then the existence of a natural number $m>0$ , nonnegative weights $w_0,\ldots,w_{m-1}$ summing to one, and positive semidefinite trace-one matrices $\sigma_j$ with $\sum_jw_j\sigma_j=\rho$ , such that

(\ln2)\left[ H_2\!\left(\left(\sum_jw_jq_{b|j}\right)_b\right) -\sum_jw_jH_2((q_{b|j})_b)\right] =H_{\mathrm{Hall}}(\rho,E), \quad q_{b|j}=\operatorname{Re}\operatorname{tr}(E_b\sigma_j),\quad H_2(q)=-\sum_bq_b\log_2q_b,

is equivalent to $T_bT_c=T_cT_b$ for every $b,c\in O$ . In addition, this commutation condition implies $\rho E_b=E_b\rho$ for every $b$ . Zero effects and zero ensemble weights are allowed, and the Hall sum omits outcomes of zero probability.

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