BipartiteSystem

formal source

  91/-! ## Entanglement Entropy -/
  92
  93/-- A bipartite quantum system. -/
  94structure BipartiteSystem where
  95  /-- Hilbert space dimension of subsystem A. -/
  96  dim_A : ℕ
  97  /-- Hilbert space dimension of subsystem B. -/
  98  dim_B : ℕ
  99  /-- Both are non-trivial. -/
 100  dim_A_pos : dim_A > 1
 101  dim_B_pos : dim_B > 1
 102
 103/-- The entanglement entropy of subsystem A.
 104    S_A = -Tr(ρ_A log ρ_A) -/
 105noncomputable def entanglementEntropy (sys : BipartiteSystem) (eigenvalues : Fin sys.dim_A → ℝ)
 106    (normalized : (Finset.univ.sum eigenvalues) = 1)
 107    (nonneg : ∀ i, eigenvalues i ≥ 0) : ℝ :=
 108  -Finset.univ.sum fun i =>
 109    if h : eigenvalues i > 0 then
 110      eigenvalues i * Real.log (eigenvalues i)
 111    else 0
 112
 113/-- **THEOREM**: Entanglement entropy is non-negative. -/
 114theorem entanglement_entropy_nonneg (sys : BipartiteSystem) (eigenvalues : Fin sys.dim_A → ℝ)
 115    (normalized : (Finset.univ.sum eigenvalues) = 1)
 116    (nonneg : ∀ i, eigenvalues i ≥ 0) :
 117    entanglementEntropy sys eigenvalues normalized nonneg ≥ 0 := by
 118  unfold entanglementEntropy
 119  simp only [neg_nonneg]
 120  apply Finset.sum_nonpos
 121  intro i _
 122  by_cases h : eigenvalues i > 0
 123  · simp only [h, dite_true]
 124    have hle : eigenvalues i ≤ 1 := by