`BookProof.ChapterMaxEntropy.entropy_eq_log_card_iff` [Nonempty α] {p : α → ℝ} (hp : IsProb p) : entropy p = Real.log (Fintype.card α) ↔ p = uniform α

Initializing...

`BookProof.ChapterMaxEntropy.entropy_eq_log_card_iff` [Nonempty α] {p : α → ℝ} (hp : IsProb p) : entropy p = Real.log (Fintype.card α) ↔ p = uniform α · Prove2Me