Sub-additivity of entropy for Bernoulli product measures

DefinitionFunction \(x \log x\) with \(0 \log 0 = 0\)#✓fully proved

The function x ↦ x log x (with 0 log 0 = 0). It equals -Real.negMulLog x (esd_Phi_eq_neg_negMulLog).

noncomputable def esd_Phi (x : ℝ) : ℝ := x * Real.log x

Used by 5

Used byData-processing inequality for entropy under a two-point mixture · Entropy of a function under a product weight · Conditional entropy in one coordinate · \(x \log x\) is the negation of Mathlib's \(-x \log x\) · Sub-additivity (tensorization) of entropy

Theorem\(x \log x\) is the negation of Mathlib's \(-x \log x\)#✓fully proved

esd_Phi is the negative of Mathlib's Real.negMulLog.

theorem esd_Phi_eq_neg_negMulLog (x : ℝ) : esd_Phi x = -Real.negMulLog x

Uses 1

Statement usesFunction \(x \log x\) with \(0 \log 0 = 0\)

DefinitionEntropy of a function under a product weight#✓fully proved

The entropy Ent_ν(g) = 𝔼_ν[g log g] - 𝔼_ν[g] log 𝔼_ν[g] of g under the product weight ν.

noncomputable def esd_ent (ν : E → Bool → ℝ) (g : ConfigSpace E → ℝ) : ℝ :=
  OSSS.expect ν (fun ω => esd_Phi (g ω)) - esd_Phi (OSSS.expect ν g)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Expectation under a product weight · Function \(x \log x\) with \(0 \log 0 = 0\)

Used bySub-additivity (tensorization) of entropy

DefinitionConditional entropy in one coordinate#✓fully proved

The conditional entropy of g in coordinate e given the other coordinates, under the Bernoulli(p) weight: p Φ(g(ω^{e↦1})) + (1-p) Φ(g(ω^{e↦0})) - Φ(𝔼[g | ω_{≠e}]), with Φ(x) = x log x.

noncomputable def esd_entCoord (p : ℝ) (g : ConfigSpace E → ℝ) (e : E) (ω : ConfigSpace E) : ℝ :=
  p * esd_Phi (g (StatMech.setOpen e ω)) + (1 - p) * esd_Phi (g (StatMech.setClosed e ω))
    - esd_Phi (OSSS.condMean (OSSS.bernoulliWeight p) e g ω)

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product weight · Conditional expectation given the other coordinates · Function \(x \log x\) with \(0 \log 0 = 0\) · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used bySub-additivity (tensorization) of entropy

DefinitionStrictly positive coordinate weights#✓fully proved

Every coordinate weight of ν is strictly positive.

def esd_PosWeight (ν : E → Bool → ℝ) : Prop := ∀ e b, 0 < ν e b

Used by 2

Used byData-processing inequality for entropy under a two-point mixture · Sub-additivity (tensorization) of entropy

TheoremData-processing inequality for entropy under a two-point mixture#✓fully proved

Data-processing inequality for entropy under a two-point mixture: for nonnegative g₀, g₁, p Φ(𝔼 g₁) + (1-p) Φ(𝔼 g₀) - Φ(p 𝔼 g₁ + (1-p) 𝔼 g₀) ≤ 𝔼[p Φ(g₁) + (1-p) Φ(g₀) - Φ(p g₁ + (1-p) g₀)].

theorem esd_dpi {μ : E → Bool → ℝ} (hpos : esd_PosWeight μ)
    (hprob : OSSS.IsProbWeight μ) {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    {g0 g1 : ConfigSpace E → ℝ} (hg0 : ∀ ω, 0 ≤ g0 ω) (hg1 : ∀ ω, 0 ≤ g1 ω) :
    p * esd_Phi (OSSS.expect μ g1) + (1-p) * esd_Phi (OSSS.expect μ g0)
        - esd_Phi (p * OSSS.expect μ g1 + (1-p) * OSSS.expect μ g0)
      ≤ OSSS.expect μ (fun ω => p * esd_Phi (g1 ω) + (1-p) * esd_Phi (g0 ω)
          - esd_Phi (p * g1 ω + (1-p) * g0 ω))

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Product probability weight · Expectation under a product weight · Function \(x \log x\) with \(0 \log 0 = 0\) · Strictly positive coordinate weights

Proof usesLog-sum inequality · Probability of a configuration under a product weight

Used bySub-additivity (tensorization) of entropy

TheoremSub-additivity (tensorization) of entropy#✓fully proved

Sub-additivity (tensorization) of entropy for the Bernoulli(p) product measure on {0, 1}^n (see S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, 2013, Theorem 4.10): for nonnegative g, Ent(g) ≤ ∑ₑ 𝔼[Entₑ(g)].

theorem esd_subadditivity {n : ℕ} {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (g : (Fin n → Bool) → ℝ) (hg : ∀ ω, 0 ≤ g ω) :
    esd_ent (OSSS.bernoulliWeight p) g
      ≤ ∑ e : Fin n, OSSS.expect (OSSS.bernoulliWeight p) (esd_entCoord p g e)

Uses 13

Statement usesBernoulli product weight · Expectation under a product weight · Entropy of a function under a product weight · Conditional entropy in one coordinate

Proof usesConfiguration space of a statistical-mechanics model · Product probability weight · Conditional expectation given the other coordinates · Probability of a configuration under a product weight · Function \(x \log x\) with \(0 \log 0 = 0\) · Strictly positive coordinate weights · Data-processing inequality for entropy under a two-point mixture · Closing a coordinate of a configuration · Opening a coordinate of a configuration

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.