Helper

entropy_uniform_set

Section fiber_entropy

Type Lemma

Proof Lines 6

Lemma entropy_uniform_set (S : {set DomainT}) (n : nat) : #|S| = n -> (0 < n)%N -> (- \sum_(x in S) n%:R^-1 * log (n%:R^-1 : R)) = log (n%:R : R).

* Entropy unfolded: sum of uniform probabilities equals log |S|.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...