Helper

gen_uniform_VarRV_probE

Section fiber_entropy_gen

Type Lemma

Proof Lines 4

Lemma gen_uniform_VarRV_probE (var : VarT) : `Pr[VarRV = var] = K%:R^-1 :> R.

Uniform VarRV gives probability K^-1

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

No lemmas in the stats use this lemma.

Loading source code...