Main

zero_centropy_eq_deterministic1

File dumas2017dual/lib/extra_entropy.v

Section zero_centropy_eq_point_mass

Type Lemma

Proof Lines 64

Signature

Lemma zero_centropy_eq_deterministic1 (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 1: conditional entropy is zero iff Z is a 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