Entropy and asymptotics / Theorem
Concavity of conditional entropy
Theorem statement
For any ensemble of bipartite quantum states $\{p(x), \rho_{AB}^x\}$, let $\omega_{AB} := \sum_x p(x)\rho_{AB}^x$. Then, the conditional von Neumann entropy is concave: $H(A \mid B)_\omega \ge \sum_x p(x)H(A \mid B)_{\rho^x}$.
Sources
- Principles of Quantum Communication Theory: A Modern Approach
Sumeet Khatri, Mark M. Wilde, 2024
Lean context
- Lean declaration
QIT.State.conditionalEntropy_concave
Copy a short prompt with the import, Lean declaration, citations, and public source link.