Helper

dsdp_centropy1_uniform

File dumas2017dual/dsdp/dsdp_entropy.v

Section dsdp_entropy

Type Lemma

Proof Lines 20

Signature

Lemma dsdp_centropy1_uniform (v1 u1 u2 u3 s : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> `H[ VarRV | CondRV = (v1, u1, u2, u3, s) ] = log (m%:R : R).

Description

Helper: Each conditioning value gives entropy log(m). Uses centropy1_uniform_over_set directly with DSDP-specific probability lemmas.

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