`BookProof.ChapterCoherentOccupation.coherentOccupation_second_moment` (lam : ℝ) : ∑' n : ℕ, (n : ℝ) ^ 2 * coherentOccupation lam n = lam ^ 2 + lam

Initializing...

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