Classical capacity / Bound
Holevo information dimension bound
Bound statement
For any ensemble $\mathcal{E}$ of states on a finite-dimensional quantum system $B$, the Holevo information is bounded by
\[
\chi(\mathcal{E}) \le \log \dim B.
\]
Sources
- From Classical to Quantum Shannon Theory
Mark M. Wilde, 2011
Lean context
- Lean declaration
QIT.Ensemble.holevo_le_log_min_card
Copy a short prompt with the import, Lean declaration, citations, and public source link.