Entropy and asymptotics / Definition
Conditional von Neumann entropy definition
Definition statement
For a quantum state $\rho$ on a bipartite system $AB$, the conditional von Neumann entropy of $A$ given $B$ is defined as $H(A|B)_\rho := H(AB)_\rho - H(B)_\rho$.
Sources
- Quantum Information Processing with Finite Resources -- Mathematical Foundations
Marco Tomamichel, 2015
Lean context
- Lean declaration
QIT.State.conditionalEntropy
Copy a short prompt with the import, Lean declaration, citations, and public source link.