`BookProof.ChapterCoherentOccupation.coherentOccupation_hasSum_second_moment` (lam : ℝ) : HasSum (fun n : ℕ => (n : ℝ) ^ 2 * coherentOccupation lam n) (lam ^ 2 + lam)

Initializing...

`BookProof.ChapterCoherentOccupation.coherentOccupation_hasSum_second_moment` (lam : ℝ) : HasSum (fun n : ℕ => (n : ℝ) ^ 2 * coherentOccupation lam n) (lam ^ 2 + lam) · Prove2Me