Entropy and asymptotics / Definition
Umegaki relative entropy definition
Definition statement
Let $\rho$ and $\sigma$ be positive semi-definite operators on a finite-dimensional system, with nonzero $\rho$. Define $D(\rho\|\sigma)$, with trace denominator $\operatorname{Tr}\rho$, by
\[
D(\rho\|\sigma):=
\begin{cases}
\dfrac{\operatorname{Tr}\!\left(\rho(\log_2\rho-\log_2\sigma)\right)}{\operatorname{Tr}\rho},&
\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma,\\
+\infty,&\text{otherwise.}
\end{cases}
\]
Sources
- Quantum Information Processing with Finite Resources -- Mathematical Foundations
Marco Tomamichel, 2015
Lean context
- Lean declaration
QIT.relativeEntropyPSDTraceLogE
Copy a short prompt with the import, Lean declaration, citations, and public source link.