`BookProof.ChapterEntropy.invertibleProb_isEquivalent_stirling` : invertibleProb ~[atTop] (fun n : ℕ => Real.sqrt (2 * Real.pi * n) * Real.exp (-(n : ℝ)))

Initializing...

`BookProof.ChapterEntropy.invertibleProb_isEquivalent_stirling` : invertibleProb ~[atTop] (fun n : ℕ => Real.sqrt (2 * Real.pi * n) * Real.exp (-(n : ℝ))) · Prove2Me