Main

zero_centropy_eq_deterministic

File dumas2017dual/lib/extra_entropy.v

Section zero_centropy_eq_point_mass

Type Lemma

Proof Lines 29

Signature

Lemma zero_centropy_eq_deterministic (V W T: finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) : `H(Z | Y) = 0 <-> (forall y, `Pr[Y = y] != 0 -> exists! z, `Pr[Z = z | Y = y] = 1).

Description

Main lemma: conditional entropy zero means Z is a unique function of Y

Uses (0)

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

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats