Helper

point_mass_to_cond_prob

File dumas2017dual/lib/extra_entropy.v

Section zero_centropy_eq_point_mass

Type Lemma

Proof Lines 6

Signature

Lemma point_mass_to_cond_prob (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (z : W) (Hy_marginal : (`p_[% Y, Z])`1 y != 0) (Hz : (jfdist_cond0 `p_[% Y, Z] y Hy_marginal) z = 1) : `Pr[Z = z | Y = y] = 1.

Description

Helper: Point mass in conditional distribution implies conditional probability = 1

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