Main

centropy1_as_sum

Section fiber_entropy

Type Lemma

Proof Lines 8

Lemma centropy1_as_sum (c : CodomainT) : `Pr[Y = c] != 0 -> `H[X | Y = c] = - \sum_(x : DomainT) `Pr[X = x | Y = c] * log (`Pr[X = x | Y = c]).

Conditional entropy expanded as negative sum of p*log(p) over domain.

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

No lemmas in the stats use this lemma.

Loading source code...