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} \]

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source