ProbabilityTheory.IsUniform.entropy_eq

lemma IsUniform.entropy_eq [DiscreteMeasurableSpace S] {H : Finset S} {X : Ω → S} {μ : Measure Ω}    [IsProbabilityMeasure μ] (hX : IsUniform H X μ) (hX' : Measurable X) :    H[X ; μ] = log (Nat.card H) := by  have (t : S) : negMulLog ((μ.map X).real {t}) = (μ.map X).real {t} * log (Nat.card H) := by    by_cases ht : t ∈ H    · simp [negMulLog, IsUniform.measureReal_preimage_of_mem' hX hX' ht]    · simp [negMulLog, map_measureReal_apply hX' (.singleton t), hX.measureReal_preimage_of_nmem ht]  rw [entropy_eq_sum_finset' (A := H), Finset.sum_congr rfl (fun t _ ↦ this t), ← Finset.sum_mul,    sum_measureReal_singleton]  · simp [Measure.real, IsUniform.full_measure hX hX']  rw [Measure.map_apply hX' (by measurability)]  exact hX.measure_preimage_compl