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.”