Classical capacity / Theorem

Holevo-Schumacher-Westmoreland classical capacity theorem

Theorem statement

For every quantum channel $\mathcal{N}$, its classical capacity is given by the regularized Holevo-information limit$$ C(\mathcal{N}) = \lim_{n\to\infty} \frac{1}{n}\,\chi(\mathcal{N}^{\otimes n}). $$

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

Open Lean source