Helper

Pr_dsdp_sol_uniform

File dumas2017dual/dsdp/dsdp_entropy.v

Section dsdp_entropy

Type Lemma

Proof Lines 15

Signature

Lemma Pr_dsdp_sol_uniform (u1 u2 u3 v1 s : msg) (v2 v3 : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> (v2, v3) \in dsdp_fiber u1 u2 u3 v1 s -> `Pr[ VarRV = (v2, v3) | CondRV = (v1, u1, u2, u3, s) ] = m%:R^-1.

Description

Solutions have uniform probability. Instantiates cPr_uniform_fiber from entropy_fiber_zpq.v with DSDP 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