`BookProof.ChapterCoherentTemperature.thermalTemperature_eq_mean_add_half` (h : 0 ≤ nbar) : thermalTemperature nbar = (∑' n : ℕ, (n : ℝ) * thermalProb nbar n) + 1 / 2

Initializing...

`BookProof.ChapterCoherentTemperature.thermalTemperature_eq_mean_add_half` (h : 0 ≤ nbar) : thermalTemperature nbar = (∑' n : ℕ, (n : ℝ) * thermalProb nbar n) + 1 / 2 · Prove2Me