Shearer's entropy inequality

DefinitionMarginal on a set of coordinates#✓fully proved

Let \(\alpha\) be a finite type, \(n\) a natural number and \(\mu\) a real-valued function on the strings \(x = (x_0, \dots, x_{n-1}) \in \alpha^n\). For a set \(S \subseteq \{0, \dots, n-1\}\) of coordinates, write \(x|_S : S \to \alpha\) for the restriction of a string \(x\) to \(S\). For a map \(y : S \to \alpha\), the \(S\)-marginal of \(\mu\) at \(y\) is the sum \(\sum_{x \in \alpha^n,\ x|_S = y} \mu(x)\) of \(\mu(x)\) over all strings \(x\) with \(x|_S = y\).

def shearerMarginal {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (S : Finset (Fin n)) (y : ↥S → α) : ℝ :=
  ∑ x : (Fin n → α), if (fun s : ↥S => x s.val) = y then μ x else 0

Used by 7

Used byMarginal entropy · Marginal entropy on the empty set vanishes · Monotonicity of marginal entropy · Submodularity of marginal entropy · Marginal entropy on all coordinates is the full entropy · Marginals of a nonnegative function are nonnegative · Marginals preserve total mass

DefinitionJoint entropy#✓fully proved

For a finite set \(\alpha\), a natural number \(n\) and a real-valued function \(\mu\) on \(\alpha^n\), the full (joint) entropy of \(\mu\) is \(H(\mu) = -\sum_{x \in \alpha^n} \mu(x) \log \mu(x)\), where \(\log t\) is the natural logarithm of \(|t|\) for \(t \neq 0\) and \(\log 0 = 0\).

noncomputable def shearerFullEntropy {n : ℕ} {α : Type*} [Fintype α]
    (μ : (Fin n → α) → ℝ) : ℝ :=
  -∑ x : (Fin n → α), μ x * Real.log (μ x)

Used by 3

Used byShearer's entropy inequality · Shearer's entropy inequality for every cover multiplicity · Marginal entropy on all coordinates is the full entropy

DefinitionMarginal entropy#✓fully proved

For a finite set \(\alpha\), a natural number \(n\), a real-valued function \(\mu\) on \(\alpha^n\) and a set \(S \subseteq \{0, \dots, n-1\}\) of coordinates, let \(P_S\) be the marginal of \(\mu\) on \(S\): for \(y \in \alpha^S\), \(P_S(y)\) is the sum of \(\mu(x)\) over the \(x \in \alpha^n\) whose restriction to \(S\) is \(y\). The marginal entropy of \(\mu\) on \(S\) is \(H_S(\mu) = -\sum_{y \in \alpha^S} P_S(y) \log P_S(y)\), where \(\log t\) is the natural logarithm of \(|t|\) for \(t \neq 0\) and \(\log 0 = 0\).

noncomputable def shearerMarginalEntropy {n : ℕ} {α : Type*} [Fintype α]
    [DecidableEq α] (μ : (Fin n → α) → ℝ) (S : Finset (Fin n)) : ℝ :=
  -∑ y : (↥S → α), shearerMarginal μ S y * Real.log (shearerMarginal μ S y)

Uses 1 · Used by 6

Statement usesMarginal on a set of coordinates

Used byShearer's entropy inequality · Shearer's entropy inequality for every cover multiplicity · Marginal entropy on the empty set vanishes · Monotonicity of marginal entropy · Submodularity of marginal entropy · Marginal entropy on all coordinates is the full entropy

TheoremMarginals of a nonnegative function are nonnegative#✓fully proved

Let \(\alpha\) be a finite set, \(n\) a natural number, \(\mu\) a real-valued function on \(\alpha^n\) with \(\mu(x) \ge 0\) for all \(x\), and \(S\) a set of coordinates in \(\{0, \dots, n-1\}\). Then the marginal \(P_S\) of \(\mu\) on \(S\) satisfies \(P_S(y) \ge 0\) for every \(y \in \alpha^S\).

theorem shearerMarginal_nonneg {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (hμ : ∀ x, 0 ≤ μ x) (S : Finset (Fin n))
    (y : ↥S → α) : 0 ≤ shearerMarginal μ S y

Uses 1 · Used by 2

Statement usesMarginal on a set of coordinates

Used byMonotonicity of marginal entropy · Submodularity of marginal entropy

TheoremMarginals preserve total mass#✓fully proved

Let \(\alpha\) be a finite set, \(n\) a natural number, \(\mu\) a real-valued function on \(\alpha^n\) with \(\sum_{x \in \alpha^n} \mu(x) = 1\), and \(S\) a set of coordinates in \(\{0, \dots, n-1\}\). Then the marginal \(P_S\) of \(\mu\) on \(S\) satisfies \(\sum_{y \in \alpha^S} P_S(y) = 1\).

theorem shearerMarginal_sum {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (hμ_sum : ∑ x : (Fin n → α), μ x = 1)
    (S : Finset (Fin n)) :
    ∑ y : (↥S → α), shearerMarginal μ S y = 1

Uses 1 · Used by 2

Statement usesMarginal on a set of coordinates

Used byMarginal entropy on the empty set vanishes · Submodularity of marginal entropy

TheoremMonotonicity of marginal entropy#✓fully proved

Let \(\alpha\) be a finite set, \(n\) a natural number, and \(\mu\) a real-valued function on \(\alpha^n\) with \(\mu(x) \ge 0\) for all \(x\). If \(T \subseteq S\) are sets of coordinates in \(\{0, \dots, n-1\}\), then the marginal entropy of \(\mu\) on \(T\) is at most the marginal entropy of \(\mu\) on \(S\).

theorem shearerMarginalEntropy_mono {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (hμ : ∀ x, 0 ≤ μ x)
    (S T : Finset (Fin n)) (hTS : T ⊆ S) :
    shearerMarginalEntropy μ T ≤ shearerMarginalEntropy μ S

Uses 3 · Used by 1

Statement usesMarginal entropy

Proof usesMarginal on a set of coordinates · Marginals of a nonnegative function are nonnegative

Used byShearer's entropy inequality for every cover multiplicity

TheoremSubmodularity of marginal entropy#✓fully proved

Let \(\alpha\) be a finite set, \(n\) a natural number, and \(\mu\) a probability mass function on \(\alpha^n\), that is, \(\mu(x) \ge 0\) for all \(x\) and \(\sum_{x \in \alpha^n} \mu(x) = 1\). Writing \(H_S\) for the marginal entropy of \(\mu\) on a set \(S \subseteq \{0, \dots, n-1\}\) of coordinates, any two such sets \(A\) and \(B\) satisfy \(H_{A \cup B} + H_{A \cap B} \le H_A + H_B\).

theorem shearerMarginalEntropy_submodular {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (hμ : ∀ x, 0 ≤ μ x)
    (hμ_sum : ∑ x : (Fin n → α), μ x = 1)
    (A B : Finset (Fin n)) :
    shearerMarginalEntropy μ (A ∪ B) + shearerMarginalEntropy μ (A ∩ B)
      ≤ shearerMarginalEntropy μ A + shearerMarginalEntropy μ B

Uses 4 · Used by 1

Statement usesMarginal entropy

Proof usesMarginal on a set of coordinates · Marginals of a nonnegative function are nonnegative · Marginals preserve total mass

Used byShearer's entropy inequality for every cover multiplicity

TheoremMarginal entropy on the empty set vanishes#✓fully proved

Let \(\alpha\) be a finite set, \(n\) a natural number, and \(\mu\) a real-valued function on \(\alpha^n\) with \(\sum_{x \in \alpha^n} \mu(x) = 1\). Then the marginal entropy of \(\mu\) on the empty set of coordinates is \(0\).

theorem shearerMarginalEntropy_empty {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) (hμ_sum : ∑ x : (Fin n → α), μ x = 1) :
    shearerMarginalEntropy μ ∅ = 0

Uses 3 · Used by 1

Statement usesMarginal entropy

Proof usesMarginal on a set of coordinates · Marginals preserve total mass

Used byShearer's entropy inequality for every cover multiplicity

TheoremMarginal entropy on all coordinates is the full entropy#✓fully proved

For a finite set \(\alpha\), a natural number \(n\) and a real-valued function \(\mu\) on \(\alpha^n\), the marginal entropy of \(\mu\) on the set \(\{0, \dots, n-1\}\) of all coordinates equals the full entropy of \(\mu\).

theorem shearerMarginalEntropy_univ {n : ℕ} {α : Type*} [Fintype α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ) :
    shearerMarginalEntropy μ Finset.univ = shearerFullEntropy μ

Uses 3 · Used by 1

Statement usesJoint entropy · Marginal entropy

Proof usesMarginal on a set of coordinates

Used byShearer's entropy inequality for every cover multiplicity

TheoremShearer's entropy inequality for every cover multiplicity#✓fully proved

Let \(\alpha\) be a nonempty finite set, \(n\) a natural number, and \(\mu\) a probability mass function on \(\alpha^n\), that is, \(\mu(x) \ge 0\) for all \(x \in \alpha^n\) and \(\sum_{x \in \alpha^n} \mu(x) = 1\). Write \(H(\mu)\) for the full entropy of \(\mu\) and, for a set \(S\) of coordinates in \(\{0, \dots, n-1\}\), write \(H_S(\mu)\) for the marginal entropy of \(\mu\) on \(S\). Let \(C\) be a set of subsets of \(\{0, \dots, n-1\}\) and \(k\) a natural number, possibly \(0\), such that every coordinate lies in at least \(k\) members of \(C\). Then \(k \, H(\mu) \le \sum_{S \in C} H_S(\mu)\).

theorem shearer_entropy_inequality_general
    {n : ℕ} {α : Type*} [Fintype α] [Nonempty α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ)
    (hμ_nonneg : ∀ x, 0 ≤ μ x)
    (hμ_sum : ∑ x : (Fin n → α), μ x = 1)
    (C : Finset (Finset (Fin n))) (k : ℕ)
    (hcover : ∀ i : Fin n, k ≤ (C.filter (fun S => i ∈ S)).card) :
    (k : ℝ) * shearerFullEntropy μ ≤
      ∑ S ∈ C, shearerMarginalEntropy μ S

Uses 6 · Used by 1

Statement usesJoint entropy · Marginal entropy

Proof usesMarginal entropy on the empty set vanishes · Monotonicity of marginal entropy · Submodularity of marginal entropy · Marginal entropy on all coordinates is the full entropy

Used byShearer's entropy inequality

TheoremShearer's entropy inequality#✓fully proved

Let \(\alpha\) be a nonempty finite set, \(n\) a natural number, and \(\mu\) a probability mass function on \(\alpha^n\), that is, \(\mu(x) \ge 0\) for all \(x \in \alpha^n\) and \(\sum_{x \in \alpha^n} \mu(x) = 1\). Write \(H(\mu)\) for the full entropy of \(\mu\) and, for a set \(S\) of coordinates in \(\{0, \dots, n-1\}\), write \(H_S(\mu)\) for the marginal entropy of \(\mu\) on \(S\). Let \(C\) be a set of subsets of \(\{0, \dots, n-1\}\) and \(k \ge 1\) an integer such that every coordinate lies in at least \(k\) members of \(C\). Then \(k \, H(\mu) \le \sum_{S \in C} H_S(\mu)\).

theorem shearer_entropy_inequality
    {n : ℕ} {α : Type*} [Fintype α] [Nonempty α] [DecidableEq α]
    (μ : (Fin n → α) → ℝ)
    (hμ_nonneg : ∀ x, 0 ≤ μ x)
    (hμ_sum : ∑ x : (Fin n → α), μ x = 1)
    (C : Finset (Finset (Fin n))) (k : ℕ)
    (hk : 0 < k)
    (hcover : ∀ i : Fin n, k ≤ (C.filter (fun S => i ∈ S)).card) :
    (k : ℝ) * shearerFullEntropy μ ≤
      ∑ S ∈ C, shearerMarginalEntropy μ S

Sources

• F. R. K. Chung et al., J. Combin. Theory A 43 (1986), DOI 10.1016/0097-3165(86)90019-1. It follows from shearer_entropy_inequality_general; the hypothesis hk is unused and keeps the source's shape.

Uses 3

Statement usesJoint entropy · Marginal entropy

Proof usesShearer's entropy inequality for every cover multiplicity

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.