noncomputable def ShannonEntropy.supportFinset {S : Type u_1} [Fintype S] (p : PMF S) : Finset S

The support of a PMF on a finite type, returned as a Finset: the set of elements $s$ with $p(s) \neq 0$.

theorem ShannonEntropy.supportFinset_nonempty {S : Type u_1} [Fintype S] (p : PMF S) : (supportFinset p).Nonempty

The finset support of any PMF is nonempty.

theorem ShannonEntropy.mem_supportFinset_iff {S : Type u_1} [Fintype S] (p : PMF S) (s : S) : s ∈ supportFinset p ↔ p s ≠ 0

Membership in the finset support: $s \in \text{supportFinset}(p) \iff p(s) \neq 0$.

theorem ShannonEntropy.supportFinset_uniformOfFinset {S : Type u_1} [Fintype S] (s : Finset S) (hs : s.Nonempty) : supportFinset (PMF.uniformOfFinset s hs) = s

The support of the uniform PMF on a nonempty finset $s$ is exactly $s$.

theorem ShannonEntropy.shannonEntropy_eq_sum_support {S : Type u_1} [Fintype S] (p : PMF S) : shannonEntropy p = ∑ s ∈ supportFinset p, (p s).toReal.negMulLog

The Shannon entropy can be computed by summing over the support only: $H(p) = \sum_{s \in \text{supp}(p)} \text{negMulLog}(p(s))$.

theorem ShannonEntropy.sum_support_toReal_eq_one {S : Type u_1} [Fintype S] (p : PMF S) : ∑ s ∈ supportFinset p, (p s).toReal = 1

The probabilities on the support sum to one: $\sum_{s \in \text{supp}(p)} p(s) = 1$.

theorem ShannonEntropy.entropy_uniformOfFinset {S : Type u_1} [Fintype S] (s : Finset S) (hs : s.Nonempty) : shannonEntropy (PMF.uniformOfFinset s hs) = Real.log ↑s.card

The Shannon entropy of the uniform distribution on a nonempty finset $s$ is $\log |s|$ (the natural-log analogue of the textbook's $\log_2$ version).

theorem ShannonEntropy.entropy_eq_log_card_iff {S : Type u_1} [Fintype S] (p : PMF S) : shannonEntropy p = Real.log ↑(supportFinset p).card ↔ p = PMF.uniformOfFinset (supportFinset p) ⋯

Lemma 10.1.4 (uniform bound, equality case): $H(X) = \log |\text{supp}(X)|$ if and only if $X$ is uniform on its support.

theorem ShannonEntropy.binomial_tail_entropy_bound (n k : ℕ) (hk : 0 < k) (hkn : 2 * k ≤ n) : ∑ i ∈ Finset.range (k + 1), ↑(n.choose i) ≤ (↑n / ↑k) ^ k * (↑n / (↑n - ↑k)) ^ (n - k)

Theorem 10.1.12 (binomial tail bound, multiplicative form): For $1 \leq k \leq n/2$, $\sum_{i=0}^{k} \binom{n}{i} \leq (n/k)^k \cdot (n/(n-k))^{n-k}$.