Entropy and asymptotics / Theorem
Strong subadditivity of quantum entropy
Theorem statement
For any quantum state $\rho$ on a tripartite system $ABC$, the conditional mutual information is nonnegative: $I(A; B \mid C)_\rho \ge 0$.
Sources
- Principles of Quantum Communication Theory: A Modern Approach
Sumeet Khatri, Mark M. Wilde, 2024
Lean context
- Lean declaration
QIT.State.condMutualInfoABGivenC_nonneg
Copy a short prompt with the import, Lean declaration, citations, and public source link.