Quantum entropy

import Quantum_state

variables
(ℋ : Type) [complex_Hilbert_space ℋ]
(ρ : ℋ →ₗ[ℂ] ℋ) [quantum_state ρ]

def quantum_entropy (ρ) :=
- Tr{ρ * (log ρ)}

notation `H(`ρ`)` := quantum_entropy ρ

“Alice makes quantum state |ψ y⟩. According to rnd_var pY. Before Bob receives the state from Alice, the expected density operator from his point of view is then σ = ∑ y, (pY y) * |ψ y⟩⟨ψ y|.”

“H(σ) quantifies Bob’s uncertainty: H(σ) qubits is the expected information gain upon receiving and measuring the state that Alice sends.

Schumacher’s theorem: Alice needs to send Bob qubits at a rate H(σ) in order for him to be able to decode a compressed quantum state.”

import Isometry
import Shannon_entropy

theorem quantum_entropy_nonneg :
  ∀ [quantum_state ρ], quantum_entropy ρ ≥ 0 :=
sorry -- shannon_entropy_ge_zero

theorem quantum_entropy_zero_of_pure_state :
  ∀ [quantum_state ρ], pure ρ → quantum_entropy ρ = 0 :=
sorry -- shannon_entropy_zero_iff_deterministic

/-- "Entropy does not decrease under mixing"-/
theorem quantum_entropy_concave :
  quantum_entropy ρ ≥ ∑ i, (p i) * quantum_entropy (ρᵢ i) := sorry

theorem quantum_entropy_isometric_invar :
  ∀ [quantum_state ρ], ∀ [isometry U], 
    quantum_entropy (U ρ U†) = quantum_entropy ρ :=
sorry -- unitary deos not change shannon_entropy of eigenvalues

theorem quantum_entropy_additive :
  ∀ [quantum_state ρ σ], 
    quantum_entropy ρ ⊗ σ = quantum_entropy ρ + quantum_entropy σ :=
sorry -- additivity of shanon entropies of eigenvalues

References

• Wilde2011;