 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
 125      have := Finset.single_le_sum (fun j _ => nonneg j) (Finset.mem_univ i)
 126      simp at this
 127      linarith [normalized]
 128    have hlog : Real.log (eigenvalues i) ≤ 0 := Real.log_nonpos (le_of_lt h) hle
 129    have hpos : eigenvalues i ≥ 0 := le_of_lt h
 130    exact mul_nonpos_of_nonneg_of_nonpos hpos hlog
 131  · simp [h]
 132
 133/-- **THEOREM**: Maximum entanglement entropy = log(dim_A). -/
 134theorem max_entanglement_entropy (sys : BipartiteSystem) :
 135    -- For maximally entangled state, S_A = log(dim_A)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.