Quantum relative entropy

import Quantum_state

variables
(ℋ : Type) [complex_Hilbert_space ℋ]
(ρ σ : ℋ →ₗ[ℂ] ℋ)
[quantum_state ρ]
[pos_semidef σ]
[supp ρ ⊆ supp σ]

def quantum_relative_entropy (ρ) (σ) :=
Tr{ρ * [log ρ - log σ]}

notation `D(`ρ`∥`σ`)` := quantum_relative_entropy ρ σ

“Intuitive interpretation: A distance measure between quantum states. But not strictly in the mathematical sense because it is not symmetric and it does not obey a triangle inequality.”

“Quantum relative entropy is a “parent quantity” for other entropies. Quantum entropy, the Conditional quantum entropy, the Quantum mutual information, and the Conditional quantum mutual information.”

References