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

  1. A decoupling approach to the quantum capacity

    Patrick Hayden, Michal Horodecki, Andreas Winter, Jon Yard, 2007

Lean context

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source