theorem
proved
tactic proof
entanglement_entropy_nonneg
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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). -/