One-shot entropy tools / Bound
One-shot decoupling theorem
Bound statement
Let $\phi^{AA'}$ be a pure state whose marginal $\phi^A$ has full rank $\dim A$, and let $W^{A'\to BE}$ be a Stinespring isometry for a channel $N^{A'\to B}$ with environment $E$. For a subspace $R\subseteq A$ with projection $P$, choose a Haar-random unitary $U$ on $A$, set $V=\sqrt{\dim A/\dim R}\,PU$, and let $\psi^{RBE}$ be the resulting non-normalized state after applying $V$ and then $W$. Writing $\phi^{AE}=\operatorname{Tr}_B(W\phi^{AA'}W^*)$ and $\pi^R$ for the maximally mixed state on $R$, \[\mathbb{E}_U\bigl\|\psi^{RE}-\pi^R\otimes\phi^E\bigr\|_1 \le \sqrt{\dim R\,\dim E\,\operatorname{Tr}[(\phi^{AE})^2]},\] where $\|\cdot\|_1$ is the trace norm.
Sources
- A decoupling approach to the quantum capacity
Patrick Hayden, Michal Horodecki, Andreas Winter, Jon Yard, 2007
Lean context
- Import
QIT.OneShot.Decoupling- Lean declaration
QIT.hayden_oneShotDecoupling_traceNorm_expectation_le
Copy a short prompt with the import, Lean declaration, citations, and public source link.