theorem ShearerEntropy.shannonEntropy_marginal_empty {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) : ShannonEntropy.shannonEntropy (marginal p ∅) = 0

The marginal of $p$ on the empty set has zero Shannon entropy.

noncomputable def ShearerEntropy.funUnivEquiv (n : ℕ) (Ω : Type u_2) : (Fin n → Ω) ≃ (↥Finset.univ → Ω)

Canonical equivalence between functions Fin n → Ω and functions from the subtype of the universal finset to Ω.

theorem ShearerEntropy.shannonEntropy_marginal_univ {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) : ShannonEntropy.shannonEntropy (marginal p Finset.univ) = ShannonEntropy.shannonEntropy p

The marginal of $p$ on the universal finset has the same entropy as $p$ itself.

theorem ShearerEntropy.filter_le_eq_filter_val_lt_succ {n : ℕ} (i : Fin n) : {x : Fin n | x ≤ i} = {j : Fin n | ↑j < ↑i + 1}

Rewrite the filter {j : Fin n | j ≤ i} as {j : Fin n | j.val < i.val + 1}.

theorem ShearerEntropy.filter_lt_eq_filter_val_lt {n : ℕ} (i : Fin n) : {x : Fin n | x < i} = {j : Fin n | ↑j < ↑i}

Rewrite the filter {j : Fin n | j < i} as {j : Fin n | j.val < i.val}.

theorem ShearerEntropy.chain_rule_telescoping {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) : ShannonEntropy.shannonEntropy p = ∑ i : Fin n, (ShannonEntropy.shannonEntropy (marginal p {x : Fin n | x ≤ i}) - ShannonEntropy.shannonEntropy (marginal p {x : Fin n | x < i}))

The chain rule for Shannon entropy expressed as a telescoping sum of conditional entropies: $H(p) = \sum_i \bigl(H(p|_{j \le i}) - H(p|_{j < i})\bigr)$.

theorem ShearerEntropy.marginal_entropy_lower_bound {n : ℕ} {Ω : Type u_2} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) (B : Finset (Fin n)) : ∑ i ∈ B, (ShannonEntropy.shannonEntropy (marginal p {x : Fin n | x ≤ i}) - ShannonEntropy.shannonEntropy (marginal p {x : Fin n | x < i})) ≤ ShannonEntropy.shannonEntropy (marginal p B)

Lower bound on the entropy of the marginal restricted to $B$: summing the per-step conditional entropy gains for $i \in B$ stays below $H(p|_B)$. Used to prove Shearer's lemma.

theorem ShearerEntropy.shearer_entropy_inequality {n s : ℕ} {Ω : Type u_2} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) (A : Fin s → Finset (Fin n)) (k : ℕ) (hcover : CoveringCondition A k) : ↑k * ShannonEntropy.shannonEntropy p ≤ ∑ j : Fin s, ShannonEntropy.shannonEntropy (marginal p (A j))

Shearer's entropy inequality (Theorem 10.4.5): if $\{A_j\}_{j=1}^s$ covers each index at least $k$ times, then $k \cdot H(X_1,\dots,X_n) \le \sum_{j=1}^s H(X_{A_j})$.