Entropy and asymptotics / Definition
Von Neumann entropy definition
Definition statement
For a quantum state $\rho_A$ on a finite-dimensional system $A$, its von Neumann entropy is defined as $H(A)_\rho := -\operatorname{Tr}\!\bigl(\rho_A \log_2 \rho_A\bigr).$ Equivalently, it is the Shannon entropy of the eigenvalues of $\rho_A$.
Sources
- Quantum Information Processing with Finite Resources -- Mathematical Foundations
Marco Tomamichel, 2015
Lean context
- Lean declaration
QIT.State.vonNeumann
Copy a short prompt with the import, Lean declaration, citations, and public source link.