The Helstrom bound — minimum-error state discrimination (K3) #
Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).
The operational meaning of the trace distance: it is exactly the advantage, over blind guessing, of the best possible measurement at telling two states apart.
One of two states is prepared, ρ₀ with prior p₀ and ρ₁ with prior p₁, and we must
guess which. The most general strategy is a two-outcome test — an effect E with
0 ≤ E ≤ 1 (IsTest) — where outcome E means "guess ρ₀" and outcome 1 − E means
"guess ρ₁". Helstrom's theorem says the optimal success probability is
P_success = ½ (1 + ‖p₀ρ₀ − p₁ρ₁‖₁), equivalently P_error = ½ (1 − ‖p₀ρ₀ − p₁ρ₁‖₁),
and — the sharper half — that the optimum is attained, by the projector onto the positive
eigenspace of the Helstrom operator A = p₀ρ₀ − p₁ρ₁ (helstromTest).
At equal priors this reads P_error = ½ (1 − D(ρ₀, ρ₁)) with D the trace distance of
TraceDistance.lean: indistinguishable states (D = 0) force a coin
flip, perfectly distinguishable ones (D = 1) allow an error-free test. This is the operational
content that makes traceDist the metric of statistical distinguishability, and it is the
converse companion to the data-processing inequality channel_traceDist_le
(DataProcessing.lean): channels cannot increase distinguishability,
and distinguishability is exactly what a measurement can extract.
What this file proves #
re_trace_posPart_eq—Re Tr(A₊) = ½(‖A‖₁ + Re Tr A), the Jordan-decomposition identity that converts the variational optimum into a trace norm.re_trace_mul_le_helstrom— optimality: no test beatshelstromTest,Re Tr(A·E) ≤ Re Tr(A·helstromTest)for everyEwith0 ≤ E ≤ 1.re_trace_mul_helstrom— attainment:Re Tr(A·helstromTest) = ½(‖A‖₁ + Re Tr A).successProb_le/successProb_helstromTest— the equal-prior Helstrom boundP_success ≤ ½(1 + D(ρ₀,ρ₁)), with equality athelstromTest.errorProb_ge/errorProb_helstromTest— the same in error form,P_error ≥ ½(1 − D(ρ₀,ρ₁)), attained.helstrom_indistinguishable/helstrom_perfect— the two extremes:D = 0forcesP_error = ½(a coin flip),D = 1permitsP_error = 0.successProbPrior_le/successProbPrior_helstromTest— the general-prior statementP_success ≤ ½(1 + ‖p₀ρ₀ − p₁ρ₁‖₁), attained.
Both halves rest on the Jordan-decomposition machinery already in TraceDistance.lean:
the upper bound is re_trace_mul_le_re_trace_posPart (the variational half Re Tr(A·P) ≤ Re Tr(A₊) for 0 ≤ P ≤ 1) and the attainment is mul_posProj_eq_posPart
(A · P₊ = A₊) — the positive-eigenspace projector is exactly where that bound is tight.
Relation to unambiguous discrimination #
Empirical/QM/USD.lean solves the complementary problem: zero error at the cost of a third,
inconclusive outcome. Helstrom is the two-outcome optimum — always conclusive, minimum error.
The two are the endpoints of the discrimination trade-off, and both are POVM statements.
References #
specs/qi-qec-roadmap.md (K3, the trace-distance metric core); specs/future-work.md;
specs/BACKLOG.md. Helstrom, Quantum Detection and Estimation Theory (1976);
Holevo (1973); Nielsen & Chuang §9.2.1. Companion results: QuantumInfo.traceDist
(TraceDistance.lean), QuantumInfo.channel_traceDist_le (DataProcessing.lean),
CSD.Empirical.QM.USD.usd_success (Empirical/QM/USD.lean).
Two-outcome tests #
A two-outcome test (binary POVM): an effect E with 0 ≤ E ≤ 1. Outcome E is read
as "guess the first state", outcome 1 − E as "guess the second".
- nonneg : E.PosSemidef
0 ≤ E. - le_one : (1 - E).PosSemidef
E ≤ 1.
Instances For
The Helstrom test for a Hermitian operator A: the projector onto the positive
eigenspace of A. This is the optimal discriminator for the Helstrom operator
A = p₀ρ₀ − p₁ρ₁ (re_trace_mul_le_helstrom, re_trace_mul_helstrom).
Equations
Instances For
The Helstrom test is a genuine two-outcome test.
The variational optimum #
Re Tr(A₊) = ½(‖A‖₁ + Re Tr A). Adding the Jordan decomposition
Tr A = Tr A₊ − Tr A₋ to the trace-norm identity ‖A‖₁ = Tr A₊ + Tr A₋ eliminates A₋.
This is what turns the variational optimum below into a trace norm.
Optimality of the Helstrom test. For every two-outcome test E,
Re Tr(A·E) ≤ Re Tr(A·helstromTest) — no measurement extracts more of A than the
projector onto its positive eigenspace.
Attainment. The Helstrom test achieves the bound in closed form:
Re Tr(A·helstromTest) = ½(‖A‖₁ + Re Tr A).
Equal priors: the operational meaning of the trace distance #
The success probability of the test E at discriminating ρ₀ from ρ₁, each
prepared with prior ½: guess "0" on outcome E, "1" on outcome 1 − E.
Equations
Instances For
The error probability of the test E.
Equations
- QuantumInfo.errorProb ρ₀ ρ₁ E = 1 - QuantumInfo.successProb ρ₀ ρ₁ E
Instances For
Success rewritten around the Helstrom operator ρ₀ − ρ₁: blind guessing (½) plus
half of what the test extracts from the difference.
The Helstrom bound (equal priors). No two-outcome test discriminates ρ₀ from ρ₁
better than ½(1 + D(ρ₀,ρ₁)), where D is the trace distance.
Attainment (equal priors). The Helstrom test meets the bound exactly, so
½(1 + D(ρ₀,ρ₁)) is the optimal success probability, not merely an upper bound.
The minimum error probability is ½(1 − D(ρ₀,ρ₁)) — attained by the Helstrom test.
This is the operational meaning of the trace distance.
The two extremes #
Indistinguishable states force a coin flip. If D(ρ₀,ρ₁) = 0 — equivalently
ρ₀ = ρ₁, by traceDist_eq_zero_iff — then the error probability is exactly ½ for
every E whatsoever (not merely every test): no measurement does better than guessing.
Perfectly distinguishable states admit an error-free test. If D(ρ₀,ρ₁) = 1 then the
Helstrom test has error probability 0.
General priors #
The success probability at general priors p₀, p₁: guess "0" on E, "1" on 1 − E.
Equations
Instances For
Success at general priors, rewritten around the Helstrom operator
A = p₀ρ₀ − p₁ρ₁: the blind-guess baseline p₁ plus what the test extracts from A.
The Helstrom bound (general priors). With priors summing to 1, no two-outcome test
succeeds with probability better than ½(1 + ‖p₀ρ₀ − p₁ρ₁‖₁).
Attainment (general priors). The Helstrom test meets the general-prior bound.