Classical capacity / Theorem

Packing lemma (derandomized average-error corollary)

Theorem statement

Let $\{p(x),\sigma_x\}_{x\in S}$ be a finite ensemble with average state $\sigma=\sum_x p(x)\sigma_x$, let $P$ be a code subspace projector, let $\{P_x\}_{x\in S}$ be codeword subspace projectors, and let $\varepsilon,d,D$ be real parameters with $D>0$ and $\varepsilon\ge0$. Suppose that for every $x\in S$ the four packing conditions hold: $\operatorname{Tr}\{P\sigma_x\}\ge 1-\varepsilon$, $\operatorname{Tr}\{P_x\sigma_x\}\ge 1-\varepsilon$, $\operatorname{Tr}\{P_x\}\le d$, and $P\sigma P\le D^{-1}P$. Then for any nonempty finite message set $M$, there exist a code choosing one codeword from $S$ for each message and a square-root-measurement decoder POVM whose uniform-message average error is at most $2(\varepsilon + 2\sqrt{\varepsilon}) + 4(|M|-1)\, d/D$.

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

Open Lean source