Main

V3_determined

File dumas2017dual/dsdp/dsdp_entropy.v

Section functional_determination

Type Lemma

Proof Lines 18

Signature

Lemma V3_determined : V3 = compute_v3 `o [% V1, U1, U2, U3, S, V2].

Description

V3 is functionally determined by the other variables via the constraint. Given V1, U1, U2, U3, S, V2, we can compute: V3 = (S - U2*V2 - U1*V1) / U3. This is key for showing H(V2,V3|constraint) = H(V2|constraint). For Z/pqZ (ring, not field), we use: - U3 is a unit because coprime (val U3) m - Division by unit: x / y = x * y^-1 - Inverse property: y^-1 * y = 1 when y is unit

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