Helper

centropy_term_deterministic

File dumas2017dual/lib/extra_entropy.v

Section zero_centropy_eq_point_mass

Type Lemma

Proof Lines 28

Signature

Lemma centropy_term_deterministic (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) : `Pr[Y = y] != 0 -> (exists z, `Pr[Z = z | Y = y] = 1) -> `p_Y y * centropy1 `p_[% Z, Y] y = 0.

Description

Helper: if the conditional distribution Pr[Z | Y = y] is deterministic (i.e., there exists z with Pr[Z = z | Y = y] = 1), then the corresponding term in the conditional entropy sum is zero.

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