`BookProof.ChapterMaxEntropy.negMulLog_sub_le` (n : ℕ) (hn : 0 < n) {x : ℝ} (hx : 0 ≤ x) : Real.negMulLog x - x * Real.log n ≤ (n : ℝ)⁻¹

Initializing...

`BookProof.ChapterMaxEntropy.negMulLog_sub_le` (n : ℕ) (hn : 0 < n) {x : ℝ} (hx : 0 ≤ x) : Real.negMulLog x - x * Real.log n ≤ (n : ℝ)⁻¹ - x · Prove2Me