theorem ProbabilityTheory.uniformOn_apply' {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (t : Set Ω) : (ProbabilityTheory.uniformOn s).real t = ↑(Nat.card ↑(s ∩ t)) / ↑(Nat.card ↑s)

theorem ProbabilityTheory.entropy_of_uniformOn {S : Type u_1} [MeasurableSpace S] (H : Set S) [MeasurableSingletonClass S] [Finite ↑H] [Nonempty ↑H] : Hm[ProbabilityTheory.uniformOn H] = Real.log ↑(Nat.card ↑H)

The entropy of a uniform measure is the log of the cardinality of its support.