Helper

zero_entropy_eq_point_mass1

File dumas2017dual/lib/extra_entropy.v

Section zero_entropy_eq_point_mass

Type Lemma

Proof Lines 72

Signature

Lemma zero_entropy_eq_point_mass1 (V: finType) (Z : {RV P -> V}) : `H `p_Z = 0 <-> exists z, `Pr[Z = z] = 1.

Description

Zero entropy characterizes point mass distributions: H(Z) = 0 iff there exists z with Pr[Z = z] = 1. This is the deterministic case - no uncertainty means one certain outcome.

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