Classical capacity / Definition

Classical capacity of a quantum channel

Definition statement

A real rate $R$ is achievable for classical communication over a quantum channel $N$ if, for every $\varepsilon>0$ and every slack $\delta>0$, all sufficiently large blocklengths admit classical message codes over $N^{\otimes n}$ with rate at least $R-\delta$ and maximal error at most $\varepsilon$. The classical capacity is the supremum over all achievable real rates:$$ C(N) := \sup R. $$

Sources

Lean context

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

Open Lean source