Helper

fiberC_cond_Pr0

Section fiber_entropy

Type Lemma

Proof Lines 11

Lemma fiberC_cond_Pr0 (c : CodomainT) (x : DomainT) : `Pr[Y = c] != 0 -> x \notin fiber f c -> `Pr[X = x | Y = c] = 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...