Classical capacity / Definition

Holevo information

Definition statement

For a quantum channel $\mathcal{N}$, the Holevo information $\chi(\mathcal{N})$ is the supremum of the Holevo quantity over all finite input ensembles:$$ \chi(\mathcal{N}) := \sup_{\{p_X(x),\rho_x\}}\left[H\!\left(\sum_x p_X(x)\,\mathcal{N}(\rho_x)\right) - \sum_x p_X(x)\,H\!(\mathcal{N}(\rho_x))\right]\!. $$

Sources

Lean context

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

Open Lean source