Main

cPr_uniform_fiber

File dumas2017dual/entropy_fiber/entropy_fiber_zpq.v

Section conditional_probability

Type Lemma

Proof Lines 39

Signature

Lemma cPr_uniform_fiber (cond : CondT) (v : msg * msg) : `Pr[CondRV = cond] != 0 -> v \in fiber cond -> `Pr[VarRV = v | CondRV = cond] = #|fiber cond|%:R^-1.

Description

* Uniform conditional probability over fiber. Pr[VarRV = v | CondRV = cond] = |fiber(cond)|^-1 When: 1. VarRV is uniform over msg × msg 2. VarRV is independent of InputRV 3. The conditioning event has positive probability 4. v is in the fiber of cond This is the key lemma for deriving entropy bounds in protocols where the constraint creates a fiber structure.

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