Helper

uniform_VarRV_probE

Section fiber_entropy

Type Lemma

Proof Lines 4

Lemma uniform_VarRV_probE (var : msg * msg) : `Pr[VarRV = var] = (m ^ 2)%:R^-1 :> R.

Uniform VarRV gives probability (m²)^-1

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

No lemmas in the stats use this lemma.

Loading source code...