Helper

Pr_dsdp_nosol_eq0

File dumas2017dual/dsdp/dsdp_entropy.v

Section dsdp_entropy

Type Lemma

Proof Lines 17

Signature

Lemma Pr_dsdp_nosol_eq0 (u1 u2 u3 v1 s : msg) (v2 v3 : msg) : `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> (v2, v3) \notin dsdp_fiber u1 u2 u3 v1 s -> `Pr[ VarRV = (v2, v3) | CondRV = (v1, u1, u2, u3, s) ] = 0.

Description

Non-solutions have zero probability

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