`BookProof.ChapterThermalMaxEntropy.log_thermalProb` (h : 0 < nbar) (n : ℕ) : Real.log (thermalProb nbar n) = -Real.log (nbar + 1) + (n : ℝ) * Real.log (thermalRatio nbar)

Initializing...

`BookProof.ChapterThermalMaxEntropy.log_thermalProb` (h : 0 < nbar) (n : ℕ) : Real.log (thermalProb nbar n) = -Real.log (nbar + 1) + (n : ℝ) * Real.log (thermalRatio nbar) · Prove2Me