noncomputable def ShearerEntropy.marginal {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) (A : Finset (Fin n)) : PMF (↥A → Ω)

The marginal distribution of a joint PMF $p$ on Fin n → Ω restricted to coordinates in $A \subseteq \{1,\dots,n\}$.

def ShearerEntropy.CoveringCondition {n s : ℕ} (A : Fin s → Finset (Fin n)) (k : ℕ) : Prop

The covering condition for Shearer's lemma: a family $\{A_j\}_{j=1}^s$ is a $k$-cover of $\{1,\dots,n\}$ if every index appears in at least $k$ of the sets $A_j$.

theorem ShearerEntropy.marginal_comp {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) (A B : Finset (Fin n)) (hBA : B ⊆ A) : marginal p B = PMF.map (fun (f : ↥A → Ω) (i : ↥B) => f ⟨↑i, ⋯⟩) (marginal p A)

Marginal composition: when $B \subseteq A$, marginalizing $p$ onto $B$ equals marginalizing $p$ onto $A$ first and then restricting further to $B$.

theorem ShearerEntropy.shannonEntropy_map_le {S : Type u_1} {T : Type u_2} [Fintype S] [Fintype T] [DecidableEq T] (q : PMF S) (f : S → T) : ShannonEntropy.shannonEntropy (PMF.map f q) ≤ ShannonEntropy.shannonEntropy q

The Shannon entropy is non-increasing under deterministic maps: $H(f(X)) \le H(X)$.

theorem ShearerEntropy.marginal_entropy_mono {n : ℕ} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : PMF (Fin n → Ω)) (A B : Finset (Fin n)) (hBA : B ⊆ A) : ShannonEntropy.shannonEntropy (marginal p B) ≤ ShannonEntropy.shannonEntropy (marginal p A)

Monotonicity of marginal entropy: $H(p|_B) \le H(p|_A)$ whenever $B \subseteq A$.