`BookProof.ChapterCoherentOccupation.coherentOccupation_energy` (lam : ℝ) : ∑' n : ℕ, ((n : ℝ) + 1 / 2) * coherentOccupation lam n = lam + 1 / 2

Initializing...

`BookProof.ChapterCoherentOccupation.coherentOccupation_energy` (lam : ℝ) : ∑' n : ℕ, ((n : ℝ) + 1 / 2) * coherentOccupation lam n = lam + 1 / 2 · Prove2Me