Entropy and asymptotics / Theorem
Schumacher compression converse
Theorem statement
Let $\rho$ be a density operator on a finite-dimensional Hilbert space with von Neumann entropy $H(\rho)$. If $R$ is any achievable Schumacher compression rate for the i.i.d. source $\rho$ under the joint (purification) trace-distance error criterion, then $H(\rho) \le R$.
Sources
- From Classical to Quantum Shannon Theory
Mark M. Wilde, 2011
Lean context
- Lean declaration
QIT.State.schumacher_converse
Copy a short prompt with the import, Lean declaration, citations, and public source link.