Theorem

dsdp_centropy_uniform_n

File dumas2017dual/dsdp/dsdp_entropy.v

Section dsdp_entropy_n

Type Theorem

Proof Lines 22

Signature

Theorem dsdp_centropy_uniform_n : (forall t, (0 < val (u_of_cond (CondRV t) ord_max))%N) -> (forall t, (val (u_of_cond (CondRV t) ord_max) < minn p q)%N) -> `H(VarRV | CondRV) = log ((m ^ n_relay)%:R : R).

Description

Main N-party entropy result: H(V_relay | CondRV) = log(m^n_relay) where V_relay are the relay parties' private inputs.

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