Display (4), p.4 — Uhlmann: a purification $\psi_{01}$ of $\rho_B(\psi'_{0,\gamma})$ with $\langle\psi_{01}|\psi'_{1,\gamma}\rangle = \sqrt{F'(\gamma)}$

Let $A$ and $B$ be finite-dimensional systems and $\psi_0, \psi_1$ unit vectors of $A \otimes B$, with Bob's reduced states $\rho_B(\psi_b) = \operatorname{Tr}_A|\psi_b\rangle\langle\psi_b|$. Then there is a unit vector $\psi_{01}$ of $A\otimes B$ that is a purification of $\rho_B(\psi_0)$, i.e. $\rho_B(\psi_{01}) = \rho_B(\psi_0)$, such that

a real number. Since $0 \le \sqrt F \le 1$, this gives the paper's inequality (4), $\langle\psi_{01}|\psi'_{1,\gamma}\rangle \ge F'(\gamma)$, for $\psi_b = \psi'_{b,\gamma}$.

This is the attained form of Uhlmann's theorem on a fixed purifying system: the purification lives on the same Alice side on which $\psi_0$ and $\psi_1$ live, so Alice can reach it from $\psi_0$ by a unitary on her side.

Formalization Note $\langle x|y\rangle$ is inner ℂ x y, conjugate-linear in $x$. Alice's side is the first tensor factor and traceLeft gives $\rho_B$. The overlap is equated with rootFidelity, the square root of Jozsa's fidelity $F$.

Differences from the source:

• generalization: ⟨ψ01|ψ′1,γ⟩ ≥ F′(γ) (4) → inner ℂ ψ01 ψ1 = rootFidelity ρB(ψ0) ρB(ψ1) = √F, a real number; reason: 0 ≤ √F ≤ 1, so √F ≥ F and the equality implies the printed inequality
• generalization: the post-commit states ψ′0,γ, ψ′1,γ → any unit vectors ψ0, ψ1 of A ⊗ B; reason: the post-commit states are a special case
• encoding: the fidelity [9] (Jozsa) F(ρ, σ) = (Tr √(√ρ σ √ρ))² → QAlgorithms.rootFidelity ρ σ ^ 2; reason: rootFidelity is Tr √(√ρ σ √ρ); its square is Jozsa's fidelity, the one the paper cites
• encoding: H_A ⊗ H_B with Alice's side H_A → EuclideanSpace ℂ (A × B) with Alice's side the first factor A; traceLeft gives Bob's reduced state and Alice acts by Matrix.kronecker U 1; reason: fixed ordering convention of the published traceLeft; it changes no instance