Main

centropy1_uniform_over_set

File dumas2017dual/entropy_fiber/entropy_fiber.v

Section general_pointwise_entropy

Type Lemma

Proof Lines 22

Signature

Lemma centropy1_uniform_over_set (S : {set DomainT}) (c : CodomainT) : `Pr[Y = c] != 0 -> (forall x, x \in S -> `Pr[X = x | Y = c] = #|S|%:R^-1) -> (forall x, x \notin S -> `Pr[X = x | Y = c] = 0) -> (0 < #|S|)%N -> `H[X | Y = c] = log (#|S|%:R : R).

Description

General pointwise conditional entropy when distribution is uniform over a set. KEY: This does NOT require Y = f `o X - works for any relationship between X and Y, making it applicable to DSDP and other protocols where the conditioning variable is not simply a function of the variable of interest. Usage: When X is uniformly distributed over set S given Y = c, and has zero probability outside S, the conditional entropy equals log(|S|).

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