Equations (59),(60): Hall alternative accessible-information bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.hallMeasurementBound

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

prove2quantum

For any finite normalized PSD ensemble $\mathcal E$ with average $\rho$ and any finite POVM $\mathcal M=\{E_b\}$ , set $\tau_b=\operatorname{Tr}(E_b\rho)$ and, only when $\tau_b>0$ , $\sigma_b=\tau_b^{-1}\sqrt\rho E_b\sqrt\rho$ . Then

I(\mathcal E,\mathcal M)\le S(\rho)-\sum_{b:\tau_b>0}\tau_bS(\sigma_b)=\sum_{b:\tau_b>0}\tau_bH(\sigma_b,\rho).

The average may be singular; the active dual states are supported on its support. This is Hall’s alternative bound, with the probability factor retained in both sums.

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, equations (59)–(60), PDF p.21: Hall's bound with the tau_b
factor and only active normalization. The average may be singular. -/
theorem hallMeasurementBound [Nonempty A] [Nonempty J] [Nonempty O] (w : J → ℝ) (hw : IsLaw w)
    (sigma : J → Mat A) (hs : ∀ j, IsDensityMatrix (sigma j)) (E : O → Mat A) (hE : IsPOVM E) :
    (Real.log 2 * measurementInformation w sigma E) ≤ hallBound (average w sigma) E ∧
      hallBound (average w sigma) E = hallRelative (average w sigma) E := 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, Equations (59),(60): Hall alternative accessible-information 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 matrix operations, let $w_j\ge0$ with $\sum_jw_j=1$ , let every $\sigma_j$ be positive semidefinite of trace one, and let $E_b$ be positive semidefinite effects summing to $I_A$ . Set $\rho=\sum_jw_j\sigma_j$ , $p_{b|j}=\operatorname{Re}\operatorname{tr}(E_b\sigma_j)$ , $p_b=\operatorname{Re}\operatorname{tr}(E_b\rho)$ , $T_b=\rho^{1/2}E_b\rho^{1/2}$ , and $\tau_b=p_b^{-1}T_b$ , using scalar inversion with $0^{-1}=0$ . With $H_2(p)=-\sum_bp_b\log_2p_b$ and $S(X)=-\operatorname{Re}\operatorname{tr}[f(X)]$ , $f(x)=x\ln x$ applied by continuous functional calculus, one has

(\ln2)\left[H_2((p_b)_b)-\sum_jw_jH_2((p_{b|j})_b)\right] \le S(\rho)-\sum_{\substack{b\in O\\p_b>0}}p_bS(\tau_b) =\sum_{\substack{b\in O\\p_b>0}}p_bD_{\mathbb R}(\tau_b\Vert\rho).

Here $D(X\Vert Y)=\operatorname{Re}\operatorname{tr}[f(X)-X\log Y]$ when $\ker Y\subseteq\ker X$ , and $+\infty$ otherwise; real conversion to $D_{\mathbb R}$ sends $+\infty$ to zero. Logarithms use value zero at zero. The average $\rho$ may be singular, weights and effects may vanish, and both sums restricted by $p_b>0$ assign zero to the omitted terms.

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