Shannon Entropy Lemmas for BitString Distributions

This module collects reusable Shannon-entropy and statistical-distance bounds on BitString n distributions:

• Cslib.Probability.PMF.entropy_ge_of_dist_uniform: general statistical-distance-to-entropy lower bound $H(p) \ge (n - 1)(1 - 2 \cdot \mathsf{SD}(p, U_n))$.
• Cslib.Probability.PMF.entropy_ge_of_dist_uniform_le: if $\mathsf{SD}(p, U_n) \le 1 / n^2$, then $H(p) \ge n - 2$ (Liu and Pass, Lemma 2.2, §2.5, p. 9 of arXiv:2009.11514v1).
• Cslib.Probability.PMF.sum_filter_mass_le_ge_of_entropy_ge: if $H(p) \ge B \ge 3$ on BitString m ($m \ge 1$), then outcomes with point mass at most $2^{-(B - 3)}$ have total probability at least $1 / m$ (Liu and Pass, Proof of Theorem 5.2, Claim 2, §5.2, p. 12 of arXiv:2009.11514v1).
• Cslib.Probability.PMF.entropy_ofList_take_ge: truncating an m-bit distribution to its first k ≤ m bits decreases Shannon entropy by at most m - k bits.
• Cslib.Probability.PMF.entropy_append_uniform: appending k independent uniform bits to an m-bit distribution increases Shannon entropy by k bits.

References

• Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Sections 2.5 and 5.2).

theorem Cslib.Probability.PMF.entropy_ge_of_dist_uniform {n : ℕ} (hn : 1 ≤ n) (p : PMF (BitString n)) : (↑n - 1) * (1 - 2 * dist p (uniformOfFintype (BitString n))) ≤ entropy p

General statistical-distance-to-entropy lower bound. For any distribution $p$ on BitString n, the mass of outcomes with probability strictly above $2^{-(n - 1)}$ is at most $2 \cdot \mathsf{SD}(p, U_n)$, so $H(p) \ge (n - 1)(1 - 2 \cdot \mathsf{SD}(p, U_n))$.

theorem Cslib.Probability.PMF.entropy_ge_of_dist_uniform_le {n : ℕ} (p : PMF (BitString n)) (hdist : dist p (uniformOfFintype (BitString n)) ≤ 1 / ↑n ^ 2) : ↑n - 2 ≤ entropy p

Liu and Pass, Lemma 2.2, §2.5, p. 9 of arXiv:2009.11514v1: Statistical distance to uniform bounds Shannon entropy from below. If $\mathsf{SD}(p, U_n) \le 1 / n^2$, then $H(p) \ge n - 2$.

theorem Cslib.Probability.PMF.sum_filter_mass_le_ge_of_entropy_ge {m : ℕ} (hm : 1 ≤ m) (p : PMF (BitString m)) {B : ℝ} (hB : 3 ≤ B) (hent : B ≤ entropy p) : 1 / ↑m ≤ ∑ y : BitString m with (p y).toReal ≤ 2 ^ (-(B - 3)), (p y).toReal

Liu and Pass, Proof of Theorem 5.2, Claim 2, §5.2, p. 12 of arXiv:2009.11514v1: High Shannon entropy implies non-negligible mass on low-probability outcomes. For any distribution $p$ on BitString m with $m \ge 1$ and $B \ge 3$ such that $H(p) \ge B$, the set of outcomes $y$ with point mass $p(y) \le 2^{-(B - 3)}$ has total probability at least $1 / m$.

theorem Cslib.Probability.PMF.entropy_ofList_take_ge {m k : ℕ} (hk : k ≤ m) (p : PMF (BitString m)) : entropy p - ↑(m - k) ≤ entropy (PMF.map (fun (x : Fin m → Bool) => BitString.ofList k (List.take k (List.ofFn x))) p)

Truncating an m-bit distribution to its first k ≤ m bits decreases Shannon entropy by at most m - k bits.

theorem Cslib.Probability.PMF.entropy_append_uniform {m k : ℕ} (p : PMF (BitString m)) : entropy (p.bind fun (x : BitString m) => PMF.map (fun (z : Fin k → Bool) => BitString.ofList (m + k) (List.ofFn x ++ List.ofFn z)) (uniformOfFintype (BitString k))) = entropy p + ↑k

Appending k independent uniform bits to an m-bit distribution increases Shannon entropy by exactly k bits.