Entropy and asymptotics / Theorem

Schumacher quantum data-compression limit equality

Theorem statement

Let $\rho$ be a density operator on a finite-dimensional Hilbert space with von Neumann entropy $H(\rho)$. The optimal asymptotic Schumacher compression rate of the i.i.d. quantum source $\rho$, defined as the infimum over all achievable compression rates $R$, equals $H(\rho)$.

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

Open Lean source