Helper

Pr_cond_fiber_marginE

File dumas2017dual/entropy_fiber/entropy_fiber_zpq.v

Section marginal_probability

Type Lemma

Proof Lines 34

Signature

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

Description

* Marginal probability over fiber. Pr[CondRV = cond] = |fiber(cond)| × (m²)^-1 × Pr[InputRV = proj_input(cond)] This expresses the marginal probability of the conditioning event as a product of: 1. The fiber cardinality (number of solutions) 2. The uniform probability (m²)^-1 for each solution 3. The probability of the input values

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