noncomputable def Shearer.entropy {α : Type u_1} [Fintype α] (p : α → ℝ) : ℝ

Shannon entropy of a probability mass function $p : \alpha \to \mathbb{R}$: $H(p) = \sum_x -p(x) \log p(x)$.

def Shearer.marginal12 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : α × β → ℝ

The marginal of $p$ on the first two coordinates, obtained by summing out the third.

def Shearer.marginal13 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : α × γ → ℝ

The marginal of $p$ on the first and third coordinates, obtained by summing out the second.

def Shearer.marginal23 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : β × γ → ℝ

The marginal of $p$ on the second and third coordinates, obtained by summing out the first.

def Shearer.marginal1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : α → ℝ

The marginal of $p$ on the first coordinate, summing out both the second and third.

def Shearer.marginal2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : β → ℝ

The marginal of $p$ on the second coordinate, summing out both the first and third.

def Shearer.marginal3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) : γ → ℝ

The marginal of $p$ on the third coordinate, summing out both the first and second.

theorem Shearer.entropy_subadditive_two {β : Type u_1} {γ : Type u_2} [Fintype β] [Fintype γ] (q : β × γ → ℝ) (hq_nn : ∀ (x : β × γ), 0 ≤ q x) (hq_sum : ∑ x : β × γ, q x = 1) : ∑ x : β × γ, (q x).negMulLog ≤ ∑ b : β, (∑ c : γ, q (b, c)).negMulLog + ∑ c : γ, (∑ b : β, q (b, c)).negMulLog

Subadditivity of entropy for a joint distribution: $H(Y,Z) \le H(Y) + H(Z)$.

theorem Shearer.cond_sub_pointwise {β : Type u_1} {γ : Type u_2} [Fintype β] [Fintype γ] (f : β × γ → ℝ) (hf_nn : ∀ (x : β × γ), 0 ≤ f x) {m : ℝ} (hm_nn : 0 ≤ m) (hf_sum : ∑ x : β × γ, f x = m) : ∑ x : β × γ, (f x).negMulLog + m.negMulLog ≤ ∑ b : β, (∑ c : γ, f (b, c)).negMulLog + ∑ c : γ, (∑ b : β, f (b, c)).negMulLog

Pointwise conditional subadditivity: a rescaled version of entropy subadditivity expressed for a non-negative function $f$ with total mass $m$, used to derive Shearer's special case.

theorem Shearer.entropy_cond_sub_marginal1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) (hp_nn : ∀ (x : α × β × γ), 0 ≤ p x) (hp_sum : ∑ x : α × β × γ, p x = 1) : entropy p + entropy (marginal1 p) ≤ entropy (marginal12 p) + entropy (marginal13 p)

Conditional subadditivity around the first variable: $H(X,Y,Z) + H(X) \le H(X,Y) + H(X,Z)$.

theorem Shearer.entropy_cond_sub_marginal2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) (hp_nn : ∀ (x : α × β × γ), 0 ≤ p x) (hp_sum : ∑ x : α × β × γ, p x = 1) : entropy p + entropy (marginal2 p) ≤ entropy (marginal12 p) + entropy (marginal23 p)

Conditional subadditivity around the second variable: $H(X,Y,Z) + H(Y) \le H(X,Y) + H(Y,Z)$.

theorem Shearer.entropy_cond_sub_marginal3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) (hp_nn : ∀ (x : α × β × γ), 0 ≤ p x) (hp_sum : ∑ x : α × β × γ, p x = 1) : entropy p + entropy (marginal3 p) ≤ entropy (marginal13 p) + entropy (marginal23 p)

Conditional subadditivity around the third variable: $H(X,Y,Z) + H(Z) \le H(X,Z) + H(Y,Z)$.

theorem Shearer.entropy_triple_subadditive {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) (hp_nn : ∀ (x : α × β × γ), 0 ≤ p x) (hp_sum : ∑ x : α × β × γ, p x = 1) : entropy p ≤ entropy (marginal1 p) + entropy (marginal2 p) + entropy (marginal3 p)

Triple subadditivity of Shannon entropy: $H(X,Y,Z) \le H(X) + H(Y) + H(Z)$.

theorem Shearer.shearer_special_case {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] (p : α × β × γ → ℝ) (hp_nn : ∀ (x : α × β × γ), 0 ≤ p x) (hp_sum : ∑ x : α × β × γ, p x = 1) : 2 * entropy p ≤ entropy (marginal12 p) + entropy (marginal13 p) + entropy (marginal23 p)

Shearer's lemma special case (Theorem 10.4.1): $2 H(X,Y,Z) \le H(X,Y) + H(X,Z) + H(Y,Z)$.