entanglement_entropy_nonneg

formal source

 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)
 136    True := trivial
 137
 138/-! ## The Ryu-Takayanagi Formula -/
 139
 140/-- A boundary region in a holographic CFT. -/
 141structure BoundaryRegion where
 142  /-- Size of the region. -/
 143  size : ℝ
 144  /-- Size is positive. -/