How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Helstrom Binary Discrimination
Statement
Let be density operators on a finite-dimensional complex Hilbert space. If they are presented with equal prior probability, the greatest success probability of any binary measurement for identifying the state is The binary projective measurement whose first effect is the spectral projection of onto its strictly positive eigenspaces attains this value.
Facts & Assumptions
Given: Density operators and equal prior probabilities .
A finite POVM has nonnegative effects summing to and outcome probabilities (Finite POVMs and their outcome law). The current QC04 definition body is present as a draft.
For Hermitian trace-zero , its positive and negative spectral parts satisfy (Hermitian Trace Norm Positive Negative Parts). The current QC01 theorem body is present as a draft.
If are nonnegative, then by cyclicity of trace and nonnegativity (For and , , A non-negative operator has a unique non-negative square root, A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S).
Proof
Write a binary POVM as with . Its equal-prior success probability is using .
For any such effect, [L2] gives : the second trace is nonnegative by [L3], and by [L3] bounds the first by . Thus [L2] implies .
Let be the orthogonal projection onto the positive eigenspaces of . Then , so by [L2]. The binary projective measurement therefore attains the upper bound from step 1.2.
Substituting the maximum into the success formula of step 1.1 gives , as claimed.
Depends on
- Trace Distance
- Finite POVMs and their outcome law
- A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S
- A non-negative operator has a unique non-negative square root
- Hermitian Trace Norm Positive Negative Parts
- For $A\in M_{m\times n}(F)$ and $B\in M_{n\times m}(F)$, $\operatorname{tr}(AB)=\operatorname{tr}(BA)$
Used by
Dependency tree · two levels
28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- John Watrous, The Theory of Quantum Information (standard reference, not scraped)
- John Preskill, Quantum Computation, Chapter 2: Foundations I: States and Ensembles (updated July 2015) (standard reference, not scraped)