Helper

gen_Pr_cond_fiber_marginE

File dumas2017dual/entropy_fiber/entropy_fiber_zpq.v

Section gen_marginal_probability

Type Lemma

Proof Lines 34

Signature

Lemma gen_Pr_cond_fiber_marginE (cond : CondT) : `Pr[InputRV = proj_input cond] != 0 -> `Pr[CondRV = cond] = #|fiber cond|%:R * K%:R^-1 * `Pr[InputRV = proj_input cond].

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