Helper

inde_cond_entropy

Section inde_entropy_lemmas

Type Lemma

Proof Lines 7

Lemma inde_cond_entropy (U A B : finType) (P : R.-fdist U) (View : {RV P -> A}) (X : {RV P -> B}) : P |= View _|_ X -> `H(X | View) = `H `p_ X.

Independence implies conditional entropy equals unconditional: H(X|V) = H(X)

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

No lemmas in the stats use this lemma.

Loading source code...