Helper

entropy_fdist_uniform_set

File dumas2017dual/entropy_fiber/entropy_fiber.v

Section fiber_entropy

Type Lemma

Proof Lines 15

Signature

Lemma entropy_fdist_uniform_set (S : {set DomainT}) (n : nat) : #|S| = n -> (0 < n)%N -> exists (P : R.-fdist DomainT), (forall x, x \in S -> P x = n%:R^-1) -> (forall x, x \notin S -> P x = 0) -> `H P = log (n%:R : R).

Description

Note: although this is the same as the lemma above, it is difficult to use this version in the following `centropy1_uniform_fiber` proof. So both versions are kept.

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