Helper

fiberC_jcond_Pr0

Section conditional_entropy_with_functional_constraint

Type Lemma

Proof Lines 14

Lemma fiberC_jcond_Pr0 (y : YT) (z : ZT) (x : XT) : `Pr[[% Y, Z] = (y, z)] != 0 -> g x y != z -> `Pr[X = x | [% Y, Z] = (y, z)] = 0.

Helper: values outside the fiber have zero conditional probability

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

No lemmas in the stats use this lemma.

Loading source code...