Motivation

Two parties, Alice and Bob, who share many copies of a noisy entangled state can try to convert them into fewer, nearly perfect maximally entangled pairs. This is entanglement purification (or distillation). Its best rate, the distillable entanglement, determines how much quantum information can be sent through a noisy channel when classical communication is free, so upper bounds on it are upper bounds on quantum channel capacities (Bennett et al. 1996).

The physically meaningful protocols use local operations and classical communication (LOCC), one-way ($D_1$) or two-way ($D_2$). The set of LOCC protocols is hard to describe, which makes upper bounds hard to prove. Rains (arXiv:quant-ph/9707002v3) replaced LOCC by the larger and algebraically simpler class of separable superoperators, and proved a bound for that class.

Timeline. Bennett, DiVincenzo, Smolin and Wootters (1996) bounded $D_2$ of the depolarizing (Werner) state by the entanglement of formation $E(f)=H_2\big(\tfrac12+\sqrt{f(1-f)}\big)$. Rains (1997–98) proved $D_*(f)\le 1-H_2(f)$ for separable operations, which is strictly smaller than $E(f)$ for $\tfrac12<f<1$, and a version for Bell-diagonal states. Later work gave relative-entropy bounds (Vedral–Plenio 1998) and PPT bounds (Rains 1999, 2001).

Setting

Let $V$ be an $n$-qubit register held by Alice and a copy held by Bob. The depolarizing state of one pair is

$$\Delta(\epsilon)=\frac{\epsilon}{4}\,\mathrm{Id}+\frac{1-\epsilon}{2}\big(|00\rangle+|11\rangle\big)\big(\langle00|+\langle11|\big),$$

a maximally entangled pair mixed with white noise. Its entanglement fidelity with the maximally entangled state $\phi^+=\tfrac1{\sqrt2}(|00\rangle+|11\rangle)$ is $f=1-\tfrac34\epsilon$, and $\Delta_f:=\Delta(\tfrac43(1-f))$ is the depolarizing state with fidelity $f$, a density matrix for $f\in[0,1]$. For a state $\sigma$ on $W\otimes W$ with $\dim W=K$, the fidelity is $F(\sigma)=\phi^+(W)^\dagger\sigma\,\phi^+(W)$, $\phi^+(W)=K^{-1/2}\sum_i|i\rangle|i\rangle$.

Alice and Bob share $n$ pairs, the per-pair tensor power $\Delta_f^{\otimes n}$, with Alice's $k$-th qubit entangled with Bob's $k$-th qubit. A separable superoperator $\mathcal P$ from $V\otimes V$ to $W\otimes W$ is a map

$$\mathcal P(\rho)=\sum_i\big(P_i^{(1)}\otimes P_i^{(2)}\big)\rho\big(P_i^{(1)}\otimes P_i^{(2)}\big)^\dagger,\qquad \sum_i\big(P_i^{(1)}\otimes P_i^{(2)}\big)^\dagger\big(P_i^{(1)}\otimes P_i^{(2)}\big)=\mathrm{Id},$$

with Alice's operators $P_i^{(1)}$ and Bob's $P_i^{(2)}$ acting locally. Every LOCC protocol, one-way or two-way, is separable; the converse fails.

A rate $R$ is separably achievable for $\rho$ if there are separable $\mathcal P_i$ from $n_i$ pairs to $\mathbb C^{K_i}\otimes\mathbb C^{K_i}$ with $F(\mathcal P_i(\rho^{\otimes n_i}))\to1$ and $\log_2K_i/n_i\to R$. The separably distillable entanglement $D_*(\rho)$ is the largest achievable rate. In Lean it is used only through the set of achievable rates.

Formalization targets

Goal: Theorem 2

For every $f$ with $\tfrac12\le f\le1$, both of the following hold.

$$\text{(1)}\quad D_*(f)\le 1-H_2(f)=1+f\log_2f+(1-f)\log_2(1-f).$$

(2) If separable $\mathcal P_i$ act on $n_i\to\infty$ pairs and $\log_2K_i/n_i\ge R$ eventually for some $R>1-H_2(f)$, then

$$\lim_{i\to\infty}F\big(\mathcal P_i(\Delta_f^{\otimes n_i})\big)=0.$$

The goal has two clauses. Clause (1) bounds every achievable rate, including those of sequences whose block lengths do not grow. Clause (2) is a strong converse: above the bound, fidelity does not merely stay below 1 but vanishes.

Milestones, in the order of the proof

• Eq. (12): $\mathrm{Tr}_W\sum_i|P_i\rangle\langle P_i|=\mathrm{Id}(V)$.
• Eqs. (20)–(21): $F_{\mathcal P}(\Delta^{\otimes n})=\sum_jf^{n-j}(\tfrac{1-f}3)^jB_j(\mathcal P)$, where $B_j$ sums the output fidelities on the maximally entangled state twisted by Pauli products of weight $j$.
• Eq. (25): $B'(1,0,x-y,2y)=B(x,y)$ for the partial-trace enumerator $B'$.
• Eqs. (29)–(30): $B'_{\{0\}\cup S}=2^{|S|}/K$.
• Eqs. (31)–(32): $B'(u-v,Kv,x-y,2y)$ and the shadow-type $B'(v-u,u+v,y-x,x+y)$ have nonnegative coefficients.
• Eqs. (33)–(34): $B$, $(x+3y)^n-B$ and $\tfrac1K(x+3y)^n\mp S$ have nonnegative coefficients, $S(x,y)=B(\tfrac{3y-x}2,\tfrac{x+y}2)$.
• Theorem 1: $F_{\mathcal P}(f)\le1/K$ for $f\le\tfrac12$, and $D_*(f)=0$.
• Eqs. (42)–(45), made rigorous: under $0\le B_i\le\binom ni3^i$ and $B(\tfrac12,\tfrac16)\le2^{-nR}$, $B(f,\tfrac{1-f}3)\to0$ uniformly when $R>1-H_2(f)$.

Significance

Because every LOCC protocol is separable, the goal bounds $D_1(f)$ and $D_2(f)$ of the depolarizing state by $1-H_2(f)$. For $\tfrac12<f<1$ this is strictly better than the entanglement-of-formation bound, and for one-way protocols it improved the best known bounds on part of the range. Through the reduction of channel capacity to distillation, it bounds the quantum capacity of the depolarizing channel assisted by two-way classical communication. The proof also shows that methods from classical and quantum coding theory (weight enumerators, MacWilliams identities, shadow enumerators) apply to entanglement manipulation.

The result is proved in the paper, but parts of the proof are sketched. The weight-enumerator positivity of Eqs. (31)–(32) is cited to other papers, and the final estimate (42)–(45) is written with $\simeq$ and $\gtrsim$. The mission states that estimate as a precise uniform bound. The formalization therefore adds a complete machine-checked proof: the enumerator identities in the setting of superoperators, the shadow positivity, and a rigorous large-deviation step. None of these results has a machine-checked proof yet.

Difficulty

The definition of $D_*$ quantifies over all separable superoperators of every size, so no finite computation suffices. The proof converts that quantification into linear constraints on $n+1$ numbers $B_j$, and the constraint that does the work is the shadow positivity of Eq. (32). It is not a consequence of $0\le F_{\mathcal P}(E)\le1$. It needs the positivity of quantum weight enumerators for pairs of positive operators, applied to the partial traces of the Kraus vectors, and it uses the product structure of the Kraus operators. A general channel can discard its input and prepare $\phi^+$, so no bound holds for it.

The obvious approach, bounding the fidelity by a convexity or monotonicity argument for an entanglement measure, gives the entanglement-of-formation bound, which is weaker. The final step is also not a single binomial-tail estimate. It is a linear program over the $B_j$, and it needs a Neyman–Pearson comparison of $\mathrm{Bin}(n,1-f)$ with $\mathrm{Bin}(n,\tfrac12)$ that is uniform in the coefficients.

Formalization scope

Qubit registers are Fin n → Bool with false $=|0\rangle$. The first tensor factor is Alice's, and Alice's qubit $k$ is paired with Bob's qubit $k$. Output spaces are Fin K × Fin K, and $\phi^+$ uses the computational basis. Operators are complex matrices, and fidelities are real parts. A separable superoperator is a map equal on every operator to a finite normalized product Kraus map. In finite dimension finitely many terms always suffice, so this excludes nothing. Rates use Real.logb 2 K / n with $n\ge1$. $H_2$ is the binary entropy in bits (QAlgorithms.binEntropy2). Enumerators are formal polynomials (MvPolynomial), so that "nonnegative coefficients" means coefficientwise, not pointwise on the orthant. $D_*$ is never a real supremum, which would be $0$ on an unbounded set; every statement is about the set of achievable rates.

Trivializing encodings are excluded. Separability requires normalization and product Kraus operators; dropping either makes the goal false. The fidelity is checked to equal $1-\tfrac34\epsilon$ on $\Delta(\epsilon)$ and $1$ on $\phi^+$. Theorem 1 is stated for $f\in[-\tfrac12,\tfrac12]$, which contains the range $[0,\tfrac12]$ where $\Delta_f$ is a state. The literal "any $f\le\tfrac12$" is false at $f=-2$. Clause (2) assumes $n_i\to\infty$, as the paper's proof does. Without it, discarding one pair and preparing $|00\rangle$ on $\mathbb C^4\otimes\mathbb C^4$ gives fidelity $\tfrac14$ at rate 2.

The development reuses published density-matrix, Kraus-channel, Pauli and binary-entropy definitions. A full proof needs quantum weight-enumerator theory (MacWilliams identity and shadow positivity for pairs of positive operators), partial traces over qubit subsets, and a binomial large-deviation bound. The enumerator theory and the separable-superoperator layer are reusable for PPT and Rains-bound missions. Proofs of single milestones, especially Eqs. (25) and (31)–(32) and the estimate (42)–(45), are welcome on their own.

Selected references

• E. M. Rains, Entanglement purification via separable superoperators, arXiv:quant-ph/9707002v3, 1998. https://arxiv.org/abs/quant-ph/9707002v3
• C. H. Bennett, D. P. DiVincenzo, J. A. Smolin, W. K. Wootters, Mixed-state entanglement and quantum error correction, Phys. Rev. A 54, 3824, 1996. https://arxiv.org/abs/quant-ph/9604024
• E. M. Rains, Quantum weight enumerators, IEEE Trans. Inf. Theory 44, 1388, 1998. https://arxiv.org/abs/quant-ph/9612015
• E. M. Rains, Quantum shadow enumerators, IEEE Trans. Inf. Theory 45, 2361, 1999. https://arxiv.org/abs/quant-ph/9611001
• P. Shor, R. Laflamme, Quantum analog of the MacWilliams identities for classical coding theory, Phys. Rev. Lett. 78, 1600, 1997. https://arxiv.org/abs/quant-ph/9610040

Motivation

A sender encodes one bit in the quantum state of a system: $\hat\rho_0$ with probability $1-t$ and $\hat\rho_1$ with probability $t$. The receiver measures the system. How much information about the bit can any measurement extract? The answer, the accessible information $I(t)$, is the basic figure of merit of a binary quantum communication channel and the starting point of quantum channel capacities. Explicit formulas for $I(t)$ are known only in a few special cases, so what is used in practice are bounds. The most important is the upper bound of Holevo (1973), which says that a quantum system cannot convey more information than the von Neumann entropy expression $S(t)$.

This mission formalizes §3.5.1 of C. A. Fuchs's PhD thesis (University of New Mexico, 1995; arXiv:quant-ph/9601020), which simplifies Holevo's derivation and makes explicit a function $L(t)$ that lies between the two: $I(t)\le L(t)\le S(t)$.

Timeline.

• 1964: J. P. Gordon conjectures the upper bound in print.
• 1969: L. B. Levitin announces a similar but more restricted result.
• 1973: A. S. Holevo proves it for finitely many states, outcomes and dimensions (Problemy Peredachi Informatsii 9(3), 3–11; reference [5] of the thesis). The proof compares second derivatives in $t$ and needs the existence of an intermediate function, whose second derivative it bounds without computing the function.
• 1994: Jozsa, Robb and Wootters prove the "sub-entropy" lower bound.
• 1995–96: Fuchs (with C. M. Caves) obtains Holevo's intermediate second derivative by minimizing the second derivative of the mutual information over all measurements, using the symmetric-logarithmic-derivative operator of Braunstein and Caves. This identifies a measurement attached to it.

Setting

Fix a finite dimension $D$ and two density operators $\hat\rho_0,\hat\rho_1$: positive semidefinite $D\times D$ complex matrices of trace one. For $0\le t\le1$ let

$$\hat\rho=(1-t)\hat\rho_0+t\hat\rho_1,\qquad \hat\Delta=\hat\rho_1-\hat\rho_0 .$$

A measurement (POVM) is a finite family $\{\hat E_b\}$ of positive semidefinite matrices summing to the identity. Outcome $b$ has probability $p_k(b)=\mathrm{tr}(\hat\rho_k\hat E_b)$ when the state is $\hat\rho_k$, and probability $p(b)=\mathrm{tr}(\hat\rho\hat E_b)$ overall. With the Shannon information $H(q)=-\sum_b q(b)\ln q(b)$ in nats, the mutual information of the measurement is

$$J(t)=H(p)-(1-t)H(p_0)-tH(p_1),$$

and the accessible information $I(t)$ is its supremum over all measurements with any finite number of outcomes. The von Neumann entropy is $S(\hat\rho)=-\sum_j\lambda_j\ln\lambda_j$ over the eigenvalues of $\hat\rho$, and the Holevo quantity is $S(t)=S(\hat\rho)-(1-t)S(\hat\rho_0)-tS(\hat\rho_1)$.

Let $|j\rangle$ be an orthonormal eigenbasis of $\hat\rho$ with eigenvalues $\lambda_j$, and $\Delta_{jk}=\langle j|\hat\Delta|k\rangle$. The super-operator $\mathcal L_{\hat\rho}$ is

$$\mathcal L_{\hat\rho}(\hat\Delta)=\sum_{\lambda_j+\lambda_k\ne0}\frac{2}{\lambda_j+\lambda_k}\,\Delta_{jk}\,|j\rangle\langle k| ,$$

the solution of the Lyapunov equation $\tfrac12(\hat\rho X+X\hat\rho)=\hat\Delta$. The function $\Phi(x,y)=(\ln x-\ln y)/(x-y)$, with $\Phi(x,x)=1/x$, is the reciprocal of the logarithmic mean.

Formalization targets

Goal: eq. (3.167)

Let $L$ be the function with

$$L''(t)=-\mathrm{tr}\big(\hat\Delta\,\mathcal L_{\hat\rho}(\hat\Delta)\big)\ (0<t<1),\qquad L(0)=L(1)=0 .$$

Then such an $L$ exists, and for all $0\le t\le 1$,

$$I(t)\;\le\;L(t)\;\le\;S(t).$$

Milestones (the chain of §3.5.1)

1. (3.155): $J(0)=J(1)=S(0)=S(1)=0$ for every measurement.
2. (3.156): $J''(t)=-\sum_b(\mathrm{tr}\,\hat\Delta\hat E_b)^2/\mathrm{tr}\,\hat\rho\hat E_b$.
3. (3.160): $S''(t)=-\sum_{\lambda_j+\lambda_k\ne0}\Phi(\lambda_j,\lambda_k)|\Delta_{jk}|^2$.
4. (3.179)–(3.181): $\Delta_{jk}=0$ when $\lambda_j+\lambda_k=0$, and $\mathcal L_{\hat\rho}(\hat\Delta)$ is a Hermitian solution of the Lyapunov equation, for $0<t<1$.
5. (3.182): $|\mathrm{tr}(\hat\rho\hat A\mathcal L_{\hat\rho}(\hat B))|\ge\mathrm{Re}\,\mathrm{tr}(\hat\rho\hat A\mathcal L_{\hat\rho}(\hat B))=\mathrm{tr}(\hat A\hat B)$.
6. (3.183): $J''(t)\ge-\mathrm{tr}(\mathcal L_{\hat\rho}(\hat\Delta)\hat\rho\mathcal L_{\hat\rho}(\hat\Delta))=-\mathrm{tr}(\hat\Delta\mathcal L_{\hat\rho}(\hat\Delta))=-\sum\frac{2}{\lambda_j+\lambda_k}|\Delta_{jk}|^2$.
7. (3.189): $\Phi(x,y)\ge 2/(x+y)$ for $x,y>0$, with equality iff $x=y$.
8. (3.188): $\sum\Phi(\lambda_j,\lambda_k)|\Delta_{jk}|^2\ge\sum\frac{2}{\lambda_j+\lambda_k}|\Delta_{jk}|^2$, i.e. $S''\le L''$.

Significance

The result. The outer inequality $I(t)\le S(t)$ is the Holevo bound for a binary channel. It caps the classical information a quantum system can carry and underlies the Holevo–Schumacher–Westmoreland capacity theorem. The intermediate function $L(t)$ is a tighter upper bound, given by an explicit second-order equation in terms of the Lyapunov solution $\mathcal L_{\hat\rho}(\hat\Delta)$. The eigenbasis of that operator is the measurement used for the lower bound $M(t)$ of §3.5.2. The milestones are reusable on their own: (3.160) is the second-derivative formula for the von Neumann entropy along a line of states, (3.181)–(3.182) the basic facts about the symmetric logarithmic derivative used in quantum estimation, and (3.189) the logarithmic-mean inequality.

Formalizing it. The bound $I\le S$ for general finite ensembles and POVMs, in bits, is already proved on the platform (QAlgorithms.Papers.Independent.Renew46.P35.cq_identity_and_holevo), and its equality criterion is an open goal there (…Renew46.P35.accessible_eq_holevo_iff_commuting). Neither is restated here. What is new is the intermediate function $L$ with both inequalities, and the curvature chain (3.155)–(3.189) that proves it. None of these has a machine-checked proof that we know of.

Difficulty

The obvious route is to show $J(t)\le S(t)$ directly for each measurement, but the logarithms couple $\hat\rho_0$ and $\hat\rho_1$ through $\hat\rho$, and no pointwise argument is known. The curvature argument avoids this, at three costs:

• Matrix calculus. Differentiating $S(\hat\rho)$ twice in $t$ needs a Daleckii–Krein-type formula for $\mathrm{tr}f(\hat\rho_0+t\hat\Delta)$ with $f(x)=-x\ln x$. This $f$ is not smooth at $0$, so the kernel of $\hat\rho$ has to be handled by hand: (3.179) shows it does not move for $0<t<1$.
• Singular states. $\mathcal L_{\hat\rho}$ is defined only on the support of $\hat\rho$. That $\hat\Delta$ lies in this domain uses $0<t<1$ in an essential way.
• Endpoints. $\mathrm{tr}(\hat\Delta\mathcal L_{\hat\rho}(\hat\Delta))$ can blow up like $1/t$ as $t\to0$. So $L$ is defined by a boundary value problem with a singular right-hand side. Its existence, and the passage from $J''\ge L''\ge S''$ on $(0,1)$ to inequalities on $[0,1]$, need continuity at the endpoints rather than bounds on second derivatives.

Formalization scope

Operators are Matrix d d ℂ over an arbitrary finite type d. States satisfy WildeQIT.IsDensityOperator (positive semidefinite, trace one). Measurements are families E : Fin m → Matrix d d ℂ with IsPOVM E, for any m. All entropies are in nats, with Real.negMulLog giving $0\ln0=0$. The accessible information is an sSup over every POVM, and the set of values is nonempty (the one-outcome POVM). Eigenvalues and matrix elements use Mathlib's IsHermitian.eigenvalues and eigenvectorUnitary; every quantity built from them is independent of the choice of eigenbasis. $\Phi$ is its closed form (3.162)–(3.163).

Second derivatives are stated as DifferentiableAt together with HasDerivAt (deriv f) on the open interval $(0,1)$. The predicate IsIntermediateL asks $L$ to be continuous on $[0,1]$ and twice differentiable on $(0,1)$ with $L''=-\mathrm{Re}\,\mathrm{tr}(\hat\Delta\mathcal L_{\hat\rho}(\hat\Delta))$ there, and to vanish at $0$ and $1$. The goal asserts that such an $L$ exists, which excludes a vacuous statement, and that every such $L$ (it is unique) satisfies the two bounds. No invertibility of $\hat\rho_0$ or $\hat\rho_1$ is assumed anywhere.

A complete development needs:

• second derivatives of spectral functions of a Hermitian matrix-valued path;
• the maximum principle for convex functions vanishing at the endpoints of an interval;
• the existence of a solution of $L''=-g$, $L(0)=L(1)=0$, for a continuous $g\ge0$ on $(0,1)$ dominated by the curvature of a concave function continuous on $[0,1]$.

The first and third are reusable well beyond this mission. Contributions are welcome on each milestone, on these general lemmas, and on alternative routes to the goal.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD thesis, University of New Mexico, 1995. arXiv:quant-ph/9601020
• A. S. Holevo, Bounds for the quantity of information transmitted by a quantum communication channel, Problemy Peredachi Informatsii 9(3), 3–11, 1973 (English: Problems of Information Transmission 9, 177–183). Cited as [5] in arXiv:quant-ph/9601020
• C. A. Fuchs and C. M. Caves, Ensemble-dependent bounds for accessible information in quantum mechanics, Physical Review Letters 73, 3047–3050, 1994. doi:10.1103/PhysRevLett.73.3047
• S. L. Braunstein and C. M. Caves, Statistical distance and the geometry of quantum states, Physical Review Letters 72, 3439–3443, 1994. doi:10.1103/PhysRevLett.72.3439
• R. Jozsa, D. Robb and W. K. Wootters, Lower bound for accessible information in quantum mechanics, Physical Review A 49, 668–677, 1994. doi:10.1103/PhysRevA.49.668

Why a criterion for continuous variable entanglement

Quantum optics generates entanglement between continuous variable systems: modes of the electromagnetic field described by quadratures $\hat x_j,\hat p_j$ with $[\hat x_j,\hat p_{j'}]=i\delta_{jj'}$, rather than qubits. Two-mode squeezed light underlies continuous variable teleportation (Furusawa et al., Science 282, 706, 1998), and the noise in such experiments (absorption, thermal photons) produces mixed states. Deciding whether a given mixed state is entangled is then a practical question. For finite dimensions the Peres–Horodecki partial transpose test settles it only in dimensions $2\times2$ and $2\times3$ (Peres, 1996; Horodecki et al., 1996). Duan, Giedke, Cirac and Zoller (arXiv:quant-ph/9908056v2) give a criterion for two modes based on a quantity measured directly in experiments, the total variance of a pair of Einstein–Podolsky–Rosen type operators. Simon proved independently that the partial transpose test is also necessary and sufficient for two-mode Gaussian states (arXiv:quant-ph/9909044).

Two modes, separable states and Gaussian states

A two-mode state is a density operator $\rho$ on $\ell^2(\mathbb N\times\mathbb N)$, a positive trace-class operator of trace one, with no cutoff on photon number. It is separable when it lies in the trace-norm closed convex hull of the product states $\rho_1\otimes\rho_2$. This hull contains every finite, countable or integral mixture of product states.

Write $\hat r=(\hat x_1,\hat p_1,\hat x_2,\hat p_2)$. For $w\in\mathbb R^4$, the quadrature $w\cdot\hat r$ has a probability law on $\mathbb R$ whose characteristic function is $t\mapsto\operatorname{tr}[\rho\exp(it\,w\cdot\hat r)]$. The variance $\langle(\Delta(w\cdot\hat r))^2\rangle_\rho\in[0,\infty]$ is the variance of this law.

A two-mode Gaussian state is a state for which there are a real symmetric $4\times4$ matrix $V$, the covariance, and a vector $m$ with

$$\operatorname{tr}[\rho\exp(iv\cdot\hat r)]=\exp\bigl(-\tfrac14v^TVv+im^Tv\bigr)\quad\text{for all }v\in\mathbb R^4.$$

The vacuum has $V=I$. Local linear unitary Bogoliubov operations (LLUBOs) act on each mode's pair $(\hat x_j,\hat p_j)$ by a real $2\times2$ matrix of determinant one, and on the covariance by the congruence $V\mapsto S^TVS$, where $S=S_1\oplus S_2$. Under LLUBOs every Gaussian state has a standard form II: $S^TVS=M_s^{II}$, the matrix with diagonal $(n_1,n_2,m_1,m_2)$ and off-diagonal entries $c_1$ between $\hat x_1,\hat x_2$ and $c_2$ between $\hat p_1,\hat p_2$, where

$$(n_1-1)(m_2-1)=(n_2-1)(m_1-1),\qquad |c_1|-|c_2|=\sqrt{(n_1-1)(m_1-1)}-\sqrt{(n_2-1)(m_2-1)}.$$

Formalization targets

Goal: Theorem 2 at full strength

Every two-mode Gaussian state has a standard form II. For every such rendering, every $a_0>0$ with $a_0^4(n_i-1)=m_i-1$ for $i=1,2$, and every sign choice $\varepsilon_i=\pm1$ with $\varepsilon_ic_i=|c_i|$, the operators $\hat u=a_0\hat x_1-(\varepsilon_1/a_0)\hat x_2$ and $\hat v=a_0\hat p_1-(\varepsilon_2/a_0)\hat p_2$ of the transformed frame satisfy

$$\rho\text{ separable}\iff\langle(\Delta\hat u)^2\rangle_\rho+\langle(\Delta\hat v)^2\rangle_\rho\ge a_0^2+\frac1{a_0^2}.$$

Milestones

Theorem 1 states that for every separable state, Gaussian or not, and every real $a\neq0$,

$$\langle(\Delta(|a|\hat x_1+\tfrac1a\hat x_2))^2\rangle_\rho+\langle(\Delta(|a|\hat p_1-\tfrac1a\hat p_2))^2\rangle_\rho\ge a^2+\frac1{a^2}.$$

The remark after it extends this to local canonical pairs (local symplectic frames, and every Weyl-regular local pair, which includes arbitrary local unitaries) and either sign. Lemmas 1 and 2 give the standard forms. The remaining milestones are the variance formula $\tfrac12w^TVw$ for Gaussian states, the passage from (16) to (17), the positivity of $M_s^{II}-I$, and the step from $S^TVS\succeq I$ to separability through a positive P-representation.

What the result gives

Theorem 2 reduces entanglement of a two-mode Gaussian state to one inequality on four parameters computed from the covariance, and the proof shows a stronger structural fact: a separable two-mode Gaussian state is a mixture of product coherent states up to local symplectic operations. The paper applies this to a two-mode squeezed state in a thermal environment, obtaining the time after which it becomes separable.

The paper's proofs are informal, and two of its printed steps need repair, so a machine-checked development has content beyond transcription. To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. The theorems are proved in the literature, and they are not formalized here yet. This mission states them with actual density operators on the infinite-dimensional space; separability is not replaced by a condition on covariance matrices.

Where the difficulty lies

Theorem 1 looks like a two-line computation with a decomposition $\rho=\sum_ip_i\rho_{i1}\otimes\rho_{i2}$, but separability here is a trace-norm closure. The variance is only lower semicontinuous, which is the wrong direction for passing a lower bound to a limit, so the argument needs a barycentric decomposition of the closed hull and care with infinite variance.

The obvious route in the 'if' direction, namely (17) implies $M_s^{II}-I\succeq0$, fails as printed. Physical renderings with some $n_i<1$ exist, and for those (17) does not give positivity. That branch needs a further local squeeze. The last step, from $S^TVS\succeq I$ to a state in the closed hull, requires an actual Gaussian mixture of coherent states, possibly with a singular mixing measure, and uniqueness of a state from its characteristic function.

Formalization scope

States are State (FockIndex 2) kernels with explicit trace class and positivity (Dependency50.P33). Quadratures are coefficient vectors indexed by QuadratureIndex 2 in the order $(\hat x_1,\hat p_1,\hat x_2,\hat p_2)$, with $\hbar=1$. Gaussian states are TwoModeGaussianDensity (Gap48.P47), with arbitrary first moments. Local symplectic matrices are Frontier30.P08.isSymplectic on $2\times2$ blocks, and the transformed quadrature of $w$ is $(Sw)\cdot\hat r$ on the original state, which is the Heisenberg form of the paper's LLUBOs. Variances take values in $[0,\infty]$.

The covariance-only formalization, in which separability is defined by $V\succeq S^{-T}S^{-1}$, or the variance is defined as $\tfrac12w^TVw$, would make the theorem a statement about matrices; both are excluded by these definitions.

Three encodings differ from the printed page and are declared on each item: (11a) is cross-multiplied, because its ratio is $0/0$ for a thermal state tensored with the vacuum; $a_0$ is given by fourth-power equations, which excludes only the states where the printed formula yields $a_0=0$; and the sign $c/|c|$ is a parameter $\varepsilon$.

A complete development needs the one-mode Weyl calculus on Fock space, the Robertson uncertainty relation for quadrature laws, a barycentric description of separable states (closedConvexHullBarycenters is posed, and open, on the platform), normal forms of $2\times2$ blocks, and the P-representation of Gaussian states. These parts are reusable for every later continuous variable mission. Contributions to any of them are welcome, as are proofs that bypass the P-representation through Simon's criterion.

Selected references

• L.-M. Duan, G. Giedke, J. I. Cirac, P. Zoller, Inseparability criterion for continuous variable systems, Phys. Rev. Lett. 84, 2722 (2000), cited here as arXiv:quant-ph/9908056v2. https://arxiv.org/abs/quant-ph/9908056v2
• R. Simon, Peres–Horodecki separability criterion for continuous variable systems, Phys. Rev. Lett. 84, 2726 (2000). https://arxiv.org/abs/quant-ph/9909044
• A. Peres, Separability criterion for density matrices, Phys. Rev. Lett. 77, 1413 (1996). https://doi.org/10.1103/PhysRevLett.77.1413
• M. Horodecki, P. Horodecki, R. Horodecki, Separability of mixed states: necessary and sufficient conditions, Phys. Lett. A 223, 1 (1996). https://doi.org/10.1016/S0375-9601(96)00706-2
• A. S. Holevo, M. E. Shirokov, R. F. Werner, Separability and entanglement-breaking in infinite dimensions, Russ. Math. Surv. 60, 359 (2005). https://arxiv.org/abs/quant-ph/0504204
• A. Furusawa et al., Unconditional quantum teleportation, Science 282, 706 (1998). https://doi.org/10.1126/science.282.5389.706

Motivation

A quantum system is prepared in one of two known states, and an observer must guess which one by measuring it. This is the simplest quantum decision problem, and its optimal error probability is the most operational way to say how distinguishable two quantum states are. It underlies the analysis of quantum hypothesis testing, of state discrimination in quantum communication and cryptography, and the operational meaning of the trace distance.

Timeline:

• 1969–1976. C. W. Helstrom derived the optimal measurement and the minimal error probability for two hypotheses by variational methods in Quantum Detection and Estimation Theory (Academic Press, 1976), building on his 1969 paper in J. Stat. Phys. (doi:10.1007/BF01007479).
• 1995. C. A. Fuchs's dissertation, Distinguishability and Accessible Information in Quantum Theory (arXiv:quant-ph/9601020), §3.2.1, re-derives Helstrom's result for arbitrary prior probabilities in an elementary way that does not use variational techniques.
• 1999. Fuchs and van de Graaf, Cryptographic distinguishability measures for quantum-mechanical states (arXiv:quant-ph/9712042), restate the equal-prior case as $\tfrac12 - \tfrac14\mathrm{tr}|\hat\rho_0 - \hat\rho_1|$.

This mission is the sixth of a series formalizing the capstone results of Fuchs's dissertation.

Setting

A density operator on a $D$-dimensional Hilbert space ($D$ finite) is a positive semidefinite $D \times D$ complex matrix $\hat\rho$ with $\mathrm{tr}\,\hat\rho = 1$. A POVM is a finite family $\{\hat E_b\}_{b=1}^m$ of positive semidefinite matrices with $\sum_b \hat E_b = \hat{\mathbb 1}$; the number $m$ of outcomes is arbitrary. Measuring $\{\hat E_b\}$ on $\hat\rho$ gives outcome $b$ with probability $\mathrm{tr}(\hat\rho\hat E_b)$.

The system is in state $\hat\rho_0$ with prior probability $\pi_0$ or in $\hat\rho_1$ with prior $\pi_1$, where $\pi_0, \pi_1 \ge 0$ and $\pi_0 + \pi_1 = 1$. For a fixed measurement, the best guess from the outcome is the classical Bayes decision, whose error is (2.11) of the source, $\sum_b \min\{\pi_0 p_0(b), \pi_1 p_1(b)\}$ with $p_i(b) = \mathrm{tr}(\hat\rho_i\hat E_b)$. The quantum error probability is its minimum over all measurements:

$$P_e(\hat\rho_0|\hat\rho_1) \equiv \min_{\{\hat E_b\}} \sum_b \min\big\{\pi_0\,\mathrm{tr}(\hat\rho_0\hat E_b),\ \pi_1\,\mathrm{tr}(\hat\rho_1\hat E_b)\big\}. \tag{3.9}$$

The Helstrom operator is the Hermitian matrix $\hat\Gamma = \pi_1\hat\rho_1 - \pi_0\hat\rho_0$ (3.12), with eigenvalues $\gamma_j$ (counted with multiplicity). In Lean, $P_e$ is FuchsThesis.Helstrom.qErrorProb, $\hat\Gamma$ is gammaOp, the Bayes error of a measurement is bayesError, and the error of a binary POVM $\{\hat E_0, \hat E_1\}$, $\pi_0\mathrm{tr}(\hat\rho_0\hat E_1) + \pi_1\mathrm{tr}(\hat\rho_1\hat E_0)$ (3.10), is binaryError.

Formalization targets

Goal: Helstrom's formula for arbitrary priors, eq. (3.23)

$$P_e(\hat\rho_0|\hat\rho_1) = \pi_0 + \sum_{\gamma_j \le 0} \gamma_j ,$$

and the minimum in (3.9) is attained by some POVM. The statement holds for every pair of density operators in every finite dimension (equal, orthogonal and singular states included) and every prior.

Milestones

1. (2.11) For probability distributions $p_0, p_1$, every Bayes decision function has error $\sum_b \min\{\pi_0p_0(b), \pi_1p_1(b)\}$ and every other decision function does strictly worse.
2. (3.11) The minimum over all POVMs equals the minimum over binary-valued POVMs of $\pi_0\mathrm{tr}(\hat\rho_0\hat E_1) + \pi_1\mathrm{tr}(\hat\rho_1\hat E_0)$; both minima exist.
3. (3.15) For a binary POVM, $P_e = \pi_0 + \mathrm{tr}(\hat\Gamma\hat E_0)$.
4. (3.18) For every $0 \le \hat E_0 \le \hat{\mathbb 1}$, $\mathrm{tr}(\hat\Gamma\hat E_0) \ge \sum_{\gamma_j\le0}\gamma_j$.
5. (3.19) In any eigenbasis of $\hat\Gamma$, an operator $0 \le \hat E_0^o \le \hat{\mathbb 1}$ with diagonal entries $1$ on $\gamma_j < 0$, $0$ on $\gamma_j > 0$ and any chosen values in $[0,1]$ on $\gamma_j = 0$ exists, and every $0 \le \hat E_0 \le \hat{\mathbb 1}$ with the diagonal entries (3.19) attains the bound (3.18).

Significance

The formula makes the optimal error probability of two-state discrimination computable from a single eigenvalue problem, and identifies the optimal measurement: measure $\hat\Gamma$ and guess $\hat\rho_0$ on a negative eigenvalue. For equal priors it gives $\tfrac12 - \tfrac14\,\mathrm{tr}|\hat\rho_0 - \hat\rho_1|$, which is the operational meaning of the trace distance, and so feeds every argument that bounds a guessing probability by a trace distance (security of key distribution, quantum hypothesis testing, continuity bounds). Within the dissertation it is the first of the optimized quantum distinguishability measures and the model for the fidelity result of Mission VII.

The result is classical and proved. On the formal side, related platform items cover special cases: an equal-prior, binary-POVM success-probability statement (QAlgorithms.Papers.Independent.Bridge50.P44.helstrom_equal_prior, open), a pure-state version (QAlgorithms.Arunachalam.helstrom_bound), and the equal-prior case $\tfrac12 - \tfrac14\mathrm{tr}|\hat\rho_0-\hat\rho_1|$ in the Fuchs–van de Graaf mission (FuchsVdGraaf.proposition_1). This mission adds arbitrary priors, measurements with any number of outcomes, the explicit eigenvalue form, attainment of the minimum, and the classical Bayes-decision lemma, as reusable statements.

Difficulty

The quantity (3.9) is a minimum over POVMs with any number of outcomes, and its summand is a pointwise minimum, not a linear function of the POVM. A first attempt that works only with two-outcome measurements proves a statement about a different quantity: the identification (3.11) of the two minima is a theorem in its own right, and it is needed in both directions. Variational arguments over the POVM set give stationarity conditions but not global optimality, which is why the source avoids them. The existence of the minimum is a separate issue: the measurements range over a union of sets indexed by the number of outcomes, which is not compact as a whole, so attainment is not automatic. Finally, the explicit value is an eigenvalue sum, so the statement is tied to the spectral decomposition of the indefinite Hermitian operator $\hat\Gamma$, and the formal statements must refer to Mathlib's eigenvalue and eigenvector API consistently.

Formalization scope

Operators are matrices Matrix n n ℂ over an arbitrary finite index type n. Density operators are the published WildeQIT.IsDensityOperator (positive semidefinite, trace one), POVMs the published FuchsVdGraaf.IsPOVM on Fin m for every m, and $\mathrm{tr}(\hat\rho\hat E_b)$ the published FuchsVdGraaf.outcomeDist, the real part of the trace. The minimum in (3.9) is the infimum of the set of values over all POVMs; the set contains the value $\min\{\pi_0, \pi_1\}$ of the one-outcome POVM $\{\hat{\mathbb 1}\}$, so the infimum is not the junk value of an empty set, and attainment is a separate conjunct of the goal. The eigenvalues of $\hat\Gamma$ are Matrix.IsHermitian.eigenvalues, with multiplicity, and $\sum_{\gamma_j\le0}\gamma_j$ is written $\sum_j \min(\gamma_j, 0)$. No restriction to two outcomes, to projective measurements, to equal priors or to invertible states is made: restricting the POVMs in (3.9) to binary ones would turn milestone (3.11) into a definition and is ruled out.

A complete development needs the spectral theorem for Hermitian matrices (in Mathlib), the trace inequality $\mathrm{tr}(AB) \ge 0$ for positive semidefinite $A$, $B$, and the diagonal-entry bounds $0 \le \langle j|\hat E|j\rangle \le 1$ for $0 \le \hat E \le \hat{\mathbb 1}$. These are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative routes to the goal (for instance through the trace norm).

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD dissertation, University of New Mexico, 1995. arXiv:quant-ph/9601020
• C. W. Helstrom, Quantum detection and estimation theory, J. Stat. Phys. 1, 231–252, 1969. doi:10.1007/BF01007479
• C. W. Helstrom, Quantum Detection and Estimation Theory, Academic Press, 1976.
• C. A. Fuchs and J. van de Graaf, Cryptographic distinguishability measures for quantum-mechanical states, IEEE Trans. Inf. Theory 45, 1216–1227, 1999. arXiv:quant-ph/9712042

Motivation

Two probability distributions $p_0$ and $p_1$ on the same finite set can be told apart only through samples. How well they can be told apart is the starting point of C. A. Fuchs's dissertation Distinguishability and Accessible Information in Quantum Theory (arXiv:quant-ph/9601020), which takes classical measures of distinguishability and later optimizes them over all quantum measurements. This mission formalizes the first of those measures and its multi-sample refinement, §2.2 of the thesis (printed pp.13–17).

The simplest measure is operational: an observer samples once from $p_0$ or $p_1$, knowing only prior probabilities $\pi_0, \pi_1$, and must guess which distribution was sampled. The smallest achievable probability of error measures how distinct the distributions are. An example due to Cover shows that this one-sample measure does not rank pairs of distributions consistently once more samples are allowed: one pair is more distinguishable after one sample, another after two. The Chernoff bound repairs this. It identifies a constant $\lambda$, independent of the priors and of the number of samples, that governs the exponential rate at which the optimal error probability decreases with the number of samples. The constant goes back to H. Chernoff (Ann. Math. Statist. 1952) and is a standard tool in hypothesis testing and information theory (Cover and Thomas, Chapter 12 of the first edition).

Setting

Fix a finite outcome set $B$ (the thesis writes $\{1,\dots,n\}$), two probability vectors $p_0, p_1 : B \to \mathbb R$ (nonnegative, summing to $1$) and priors $\pi_0, \pi_1 \ge 0$ with $\pi_0 + \pi_1 = 1$.

A decision function is a map $\delta : B \to \{0,1\}$, the observer's guess given the outcome $b$. Its probability of error is

$$P_e(\delta) = \pi_0 \sum_{b} \delta(b)\, p_0(b) + \pi_1 \sum_{b} \bigl[1-\delta(b)\bigr]\, p_1(b).$$

A Bayes decision function $\delta_B$ guesses $0$ when $\pi_0 p_0(b) > \pi_1 p_1(b)$, $1$ when $\pi_1 p_1(b) > \pi_0 p_0(b)$, and anything on ties. The Bayes error is

$$P_e = \sum_{b} \min\{\pi_0 p_0(b),\ \pi_1 p_1(b)\}.$$

With $N$ independent samplings the outcome is a string $b_1\dots b_N \in B^N$ with probability $p_i(b_1\dots b_N) = \prod_k p_i(b_k)$, and $P_e(N)$ is the Bayes error of this $N$-sample problem. Finally, for real $\alpha$,

$$F_\alpha(p_0/p_1) = \sum_{b} p_0(b)^{\alpha}\, p_1(b)^{1-\alpha}, \qquad \lambda = \inf_{0\le\alpha\le1} F_\alpha(p_0/p_1).$$

In Lean these are errorProb, IsBayesDecision, bayesError, productDist, errorProbN, renyiOverlap and chernoffConst in the namespace FuchsThesis.Chernoff; probability vectors use the published predicate CalibratedCE.Forecast.IsDist.

Formalization targets

Goal: Theorem 2.1 (Chernoff)

For all finite $B$, probability vectors $p_0, p_1$ and priors as above,

$$P_e(N) \le \lambda^{N} \quad\text{for every } N \ge 0,$$

and, if in addition $\pi_0 > 0$ and $\pi_1 > 0$,

$$\lim_{N\to\infty} P_e(N)^{1/N} = \lambda .$$

Milestones, in the order of the source

1. Eq. (2.9): every Bayes decision function minimizes $P_e(\delta)$, strictly against any decision function that is not a Bayes decision function.
2. Eqs. (2.10)–(2.11): the error probability of every Bayes decision function equals $\sum_b \min\{\pi_0 p_0(b), \pi_1 p_1(b)\}$, through the posterior form.
3. Eq. (2.23): $\min\{a,b\} \le a^\alpha b^{1-\alpha}$ for $a, b \ge 0$ and $0 \le \alpha \le 1$.
4. Eq. (2.28): for every $\alpha \in [0,1]$, $P_e(N) \le \pi_0^\alpha \pi_1^{1-\alpha} F_\alpha^N \le F_\alpha^N$, with the intermediate equalities of the printed chain.

Milestones 1 and 2 justify reading $P_e(N)$ as the optimal error; milestones 3 and 4 give the first clause of the goal.

Significance

The first clause gives an explicit, prior-free bound on the error of the best test after $N$ samples. The second shows that the bound is exponentially tight, so $\lambda$ is the exact rate: two pairs of distributions are compared by their Chernoff constants, whatever the priors and however many samples are taken. This makes $\lambda$, and $-\ln\lambda$ (the Chernoff information), a distinguishability measure in its own right; the thesis later optimizes it over quantum measurements.

The first clause is proved in the thesis in a few lines. The second clause is stated without proof ("we shall not consider it here; see instead Ref. [10]", p.17); its standard proofs (Cover and Thomas, §12.9 of the first edition) use the method of types or a tilted distribution. No formal proof of either clause is known to be on Prove2Me. A complete development yields a reusable formalization of the binary Bayes hypothesis-testing problem on finite alphabets and of its error exponent.

Difficulty

The upper bound is elementary. The asymptotic clause is the hard part: a lower bound $P_e(N) \ge c_N \lambda^N$ with $c_N^{1/N} \to 1$ is required. The obvious route, bounding each term $\min\{\pi_0 p_0, \pi_1 p_1\}$ from below by a geometric mean, fails because the inequality (2.23) goes the wrong way. A lower bound needs a set of strings carrying probability comparable to $\lambda^N$ under both hypotheses, typically the strings whose empirical distribution is close to the tilted distribution $p_{\alpha^*}(b) \propto p_0(b)^{\alpha^*} p_1(b)^{1-\alpha^*}$, together with a counting estimate for type classes. Degenerate cases add work: disjoint supports ($\lambda = 0$, $P_e(N) = 0$ for $N \ge 1$), equal distributions ($\lambda = 1$), and an optimal $\alpha$ at the boundary of $[0,1]$, where $\alpha \mapsto F_\alpha$ can be discontinuous under the convention $0^0 = 1$.

Formalization scope

• Outcomes form an arbitrary finite type; strings of length $N$ are functions Fin N → B, and $P_e(N)$ is a finite sum over them. Real powers are Real.rpow, with $0^0 = 1$.
• $\lambda$ is the infimum of $F_\alpha$ over $\alpha \in [0,1]$ (the thesis writes $\min$). With $0^0 = 1$ the minimum need not be attained: $p_0 = (1,0)$, $p_1 = (\tfrac12,\tfrac12)$ gives $F_\alpha = 2^{\alpha-1}$ for $\alpha > 0$ but $F_0 = 1$, and the Chernoff constant is the infimum $\tfrac12$.
• "Approached asymptotically" is the exponential rate $P_e(N)^{1/N} \to \lambda$; the literal $P_e(N)/\lambda^N \to 1$ is false. The asymptotic clause needs $\pi_0, \pi_1 > 0$, which the thesis omits: with $\pi_0 = 0$ and $p_0 = p_1$ the error is $0$ while $\lambda = 1$.
• $P_e(N)$ is defined as the Bayes error formula (2.11) for the $N$-sample problem, not as the error of a fixed rule; milestones (2.9) and (2.11) tie it to decision functions. A formalization in which $P_e(N)$ is the error of an arbitrary rule, or in which $\lambda$ is a free parameter, would trivialize the goal; neither is used.
• Welcome contributions: finite product-measure lemmas, a method-of-types library for finite alphabets, and a lower bound for the Bayes error by tilted distributions; these serve any error-exponent result.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD dissertation, University of New Mexico, 1995. arXiv:quant-ph/9601020v1
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23 (1952) 493–507. doi:10.1214/aoms/1177729330
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (2nd ed. 2006). doi:10.1002/047174882X

Why the quantum fidelity is studied

Two quantum states cannot in general be told apart perfectly, and how well they can be told apart depends on the measurement. Classically, the statistical overlap (Bhattacharyya coefficient) $\sum_b\sqrt{p_0(b)p_1(b)}$ of two probability distributions controls how quickly repeated samples separate them. The quantum question is which measurement makes the overlap smallest. The answer, in Fuchs's 1995 dissertation and in Fuchs and Caves, Mathematical techniques for quantum communication theory (arXiv:quant-ph/9604001), is the quantity known as the quantum fidelity.

The same closed formula had appeared earlier for other reasons:

• Bures (1969) used it in a distance on density operators.
• Uhlmann (1976) introduced its square as a generalized transition probability, and proved the theorem on purifications that bears his name.
• Jozsa (1994) proposed it as a measure of the fidelity of signals in a quantum channel.
• Fuchs (1995), Chapter 3 of arXiv:quant-ph/9601020v1, showed it is the optimum of the statistical overlap over all generalized measurements, and exhibited an optimal measurement.

Density operators, measurements and the overlap

A density operator on a $D$-dimensional complex Hilbert space, $D$ finite, is a nonnegative operator $\hat\rho$ with $\mathrm{tr}\,\hat\rho = 1$. A POVM is a finite collection $\{\hat E_b\}$ of nonnegative operators with $\sum_b\hat E_b = \hat{\mathbb 1}$; measuring it on a system in state $\hat\rho$ yields outcome $b$ with probability $p(b) = \mathrm{tr}(\hat\rho\hat E_b)$. The number of outcomes is not limited by $D$.

For a nonnegative operator $\hat A$, $\hat A^{1/2}$ is the unique nonnegative operator with $\hat A^{1/2}\hat A^{1/2} = \hat A$. The quantum fidelity of $\hat\rho_0$ and $\hat\rho_1$ is

$$F(\hat\rho_0,\hat\rho_1) = \min_{\{\hat E_b\}} \sum_b \sqrt{\mathrm{tr}\,\hat\rho_0\hat E_b}\,\sqrt{\mathrm{tr}\,\hat\rho_1\hat E_b} .$$

Formalization targets

Goal: the fidelity formula

For all density operators $\hat\rho_0, \hat\rho_1$, the minimum exists and

$$F(\hat\rho_0,\hat\rho_1) = \mathrm{tr}\sqrt{\hat\rho_1^{1/2}\hat\rho_0\hat\rho_1^{1/2}} .$$

The goal has two parts: the value of the infimum over POVMs, and a POVM attaining it.

Milestones

In the order of §3.3.1 and §3.3.2:

• Eq. (3.36): on pure states the formula is $|\langle\psi_0|\psi_1\rangle|$.
• Eq. (3.55): for every outcome and every unitary $\hat U$, $\sqrt{p_0(b)}\sqrt{p_1(b)} \ge |\mathrm{tr}(\hat U\hat\rho_0^{1/2}\hat E_b\hat\rho_1^{1/2})|$.
• Eq. (3.58): the sum over $b$, $\sum_b\sqrt{p_0(b)}\sqrt{p_1(b)} \ge |\mathrm{tr}(\hat U\hat\rho_0^{1/2}\hat\rho_1^{1/2})|$.
• Eqs. (3.60)–(3.61): $\max_{\hat U}|\mathrm{tr}(\hat U\hat A)| = \max_{\hat U}\mathrm{Re}\,\mathrm{tr}(\hat U\hat A) = \mathrm{tr}\sqrt{\hat A^\dagger\hat A}$, with polar decomposition.
• Eqs. (3.63), (3.65): every POVM has overlap at least $\mathrm{tr}\sqrt{\hat\rho_1^{1/2}\hat\rho_0\hat\rho_1^{1/2}}$.
• Eqs. (3.64), (3.67): for invertible states, the unique $\hat U_c$, and $\hat M$ is Hermitian and nonnegative.
• §3.3.1, (3.66)–(3.74): an orthonormal basis attains the value, whether or not the states are invertible.
• Eqs. (3.80)–(3.82): the two operators under the roots have the same spectrum, so the formula and $F$ are symmetric.

What the result gives

The theorem gives the closed formula an operational meaning: Uhlmann's transition probability and the Bures distance measure the classical overlap of the best measurement. The formula makes $F$ computable from the states, and it supplies the measurement explicitly. Later chapters use it in this role, in particular the no-broadcasting theorem of Chapter 4, and inequalities between trace distance and fidelity rest on it.

The result is proved in the source. No platform theorem states it; the related item QAlgorithms.Papers.Independent.Claimed50.P12.lemmaB_3 is Uhlmann's supremum over purifications, a different characterization that the source cites and does not use. This mission formalizes the measurement characterization, including the singular cases, and the matrix facts it needs.

Where the obvious argument fails

The immediate approach applies the Schwarz inequality for $\mathrm{tr}(\hat A^\dagger\hat B)$ to each term of the overlap, which gives the lower bound $|\mathrm{tr}(\hat\rho_1^{1/2}\hat\rho_0^{1/2})|$. That bound is generally not attained: equality in every term would require a POVM of orthogonal projectors onto eigenvectors of $\hat\rho_1^{1/2}\hat\rho_0^{-1/2}$, an operator that is not Hermitian when the states do not commute, so no complete orthogonal set of such eigenvectors exists. The bound must carry a free unitary, and the unitary must be the one that makes the equality conditions solvable. A second difficulty is singular states, for which the operator $\hat M$ of the invertible case does not exist.

Formalization scope

Operators are matrices Matrix n n ℂ over an arbitrary finite index type n. Density operators are WildeQIT.IsDensityOperator; POVMs are FuchsVdGraaf.IsPOVM, indexed by Fin m for every m; outcome probabilities are FuchsVdGraaf.outcomeDist, the real part of the trace. The optimum (3.27) is the published FuchsVdGraaf.qBhattacharyya, an infimum over all POVMs, under the name used by Fuchs and van de Graaf for the same quantity. Its summand is $\sqrt{p_0(b)p_1(b)}$, which equals $\sqrt{p_0(b)}\sqrt{p_1(b)}$ because the probabilities are nonnegative. Square roots are CFC.sqrt under MatrixOrder, and unitaries are Matrix.unitaryGroup n ℂ.

Defining the left side by the closed formula, or using a root fidelity on both sides, would make the goal trivial, so the left side is always the POVM optimum. Restricting to invertible states or to projective measurements is also excluded: both are part of what is proved.

The development needs polar decomposition for possibly singular square matrices, the Schwarz inequality for the trace inner product, and the spectral theorem for the attaining basis. Polar decomposition and the trace maximum (3.60) are reusable beyond this mission. Contributions of general matrix lemmas are welcome.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD dissertation, University of New Mexico, 1995. arXiv:quant-ph/9601020v1
• C. A. Fuchs and C. M. Caves, Mathematical techniques for quantum communication theory, Open Systems & Information Dynamics 3, 345–356, 1995. arXiv:quant-ph/9604001
• C. A. Fuchs and J. van de Graaf, Cryptographic distinguishability measures for quantum-mechanical states, IEEE Transactions on Information Theory 45, 1216–1227, 1999. arXiv:quant-ph/9712042
• A. Uhlmann, *The "transition probability" in the state space of a -algebra, Reports on Mathematical Physics 9, 273–279, 1976. doi:10.1016/0034-4877(76)90060-4
• R. Jozsa, Fidelity for mixed quantum states, Journal of Modern Optics 41, 2315–2323, 1994. doi:10.1080/09500349414552171
• D. Bures, An extension of Kakutani's theorem on infinite product measures to the tensor product of semifinite $w^*$-algebras, Transactions of the American Mathematical Society 135, 199–212, 1969. doi:10.2307/1995012