Skip to content

InformationTheory.Shannon.MaxEntropy.Constrained

Imports 6

Constrained maximum entropy (Cover–Thomas) #

For a pmf P : α → ℝ on a finite alphabet, the distribution maximizing Shannon entropy H(P) = ∑ x, negMulLog (P x) subject to moment constraints ∑ x, P x · f i x = c i is the Boltzmann–Gibbs exponential family

gibbsPmf f λ x := exp (∑ i, λ i · f i x) / Z(λ)

where Z(λ) = ∑ y, exp (∑ i, λ i · f i y) is the partition function. The Lagrange parameter λ is passed in as a hypothesis rather than solved for.

Main definitions #

gibbsZ — partition function Z(λ) := ∑ y, exp ⟨λ, f y⟩.
gibbsPmf — Boltzmann–Gibbs pmf x ↦ exp ⟨λ, f x⟩ / Z(λ).

Main statements #

gibbsPmf_mem_stdSimplex — gibbsPmf f λ ∈ stdSimplex ℝ α.
entropy_le_gibbs_of_constraints — under moment constraints, H(P) ≤ H(gibbsPmf f λ).
entropy_eq_gibbs_iff_of_constraints — equality holds iff P = gibbsPmf f λ.

Implementation notes #

KKT / Lagrange duality is not available in Mathlib (Mathlib/Analysis/Calculus/LagrangeMultipliers.lean notes the absence). The proof avoids this via the Gibbs + Csiszár klDivPmf algebraic-identity route:

0 ≤ klDivPmf P (gibbsPmf f λ) = −H(P) − ⟨λ, c⟩ + log Z(λ)
0 = klDivPmf (gibbsPmf f λ) (gibbsPmf f λ) = −H(gibbsPmf f λ) − ⟨λ, c⟩ + log Z(λ)

This avoids any need for ψ(λ) convexity or Lagrange-multiplier existence theory. We use CsiszarProjection.klDivPmf rather than Mathlib.MeasureTheory.Measure.Tilted because the Csiszár API (klDivPmf_nonneg, klDivPmf_self_eq_zero) is closed in the pmf world, and Real.exp / log arithmetic suffices without rnDeriv or =ᵐ arguments.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Gibbs pmf: definition and basic properties #

noncomputable def

InformationTheory.Shannon.MaxEntropyConstrained.gibbsZ

{α : Type u_1} [Fintype α] {k : ℕ} (f : Fin k → α → ℝ) (lam : Fin k → ℝ) :

Partition function Z(λ) := ∑ y, exp (∑ i, λ i · f i y). Independent def so that Real.log Z(λ) can be reused throughout the core identity.

Equations

InformationTheory.Shannon.MaxEntropyConstrained.gibbsZ f lam = ∑ y : α, Real.exp (∑ i : Fin k, lam i * f i y)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf

{α : Type u_1} [Fintype α] {k : ℕ} (f : Fin k → α → ℝ) (lam : Fin k → ℝ) :

α → ℝ

Boltzmann–Gibbs exponential family pmf, parametrized by Lagrange parameter lam : Fin k → ℝ and feature maps f : Fin k → α → ℝ:

gibbsPmf f λ x := exp (∑ i, λ i · f i x) / Z(λ).

The denominator Z(λ) (gibbsZ f lam) is the partition function.

Equations

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf f lam x = Real.exp (∑ i : Fin k, lam i * f i x) / InformationTheory.Shannon.MaxEntropyConstrained.gibbsZ f lam

Instances For

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsZ_pos

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) :

0 < gibbsZ f lam

The partition function Z(λ) is strictly positive (each summand is exp _ > 0 and there is at least one term by [Nonempty α]).

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_pos

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) (x : α) :

0 < gibbsPmf f lam x

Each component of gibbsPmf f λ is strictly positive.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_nonneg

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) (x : α) :

0 ≤ gibbsPmf f lam x

gibbsPmf f λ is non-negative pointwise (corollary of positivity).

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_sum_eq_one

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) :

∑ x : α, gibbsPmf f lam x = 1

The mass of gibbsPmf f λ sums to 1.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_mem_stdSimplex

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) :

gibbsPmf f lam ∈ stdSimplex ℝ α

gibbsPmf f λ ∈ stdSimplex ℝ α.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.log_gibbsPmf

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) (x : α) :

Real.log (gibbsPmf f lam x) = ∑ i : Fin k, lam i * f i x - Real.log (gibbsZ f lam)

Closed form for log (gibbsPmf f λ x): the numerator's exponent minus log Z(λ).

Used by

Core identity and main upper bound #

theorem

InformationTheory.Shannon.MaxEntropyConstrained.klDivPmf_gibbsPmf_eq

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (lam : Fin k → ℝ) (Q : α → ℝ) (hQ : Q ∈ stdSimplex ℝ α) :

CsiszarProjection.klDivPmf Q (gibbsPmf f lam) = -∑ x : α, (Q x).negMulLog - ∑ i : Fin k, lam i * ∑ x : α, Q x * f i x + Real.log (gibbsZ f lam)

For any Q ∈ stdSimplex on α, the KL divergence from Q to gibbsPmf f λ decomposes into negative entropy, the constraint inner product ⟨λ, 𝔼_Q[f]⟩, and log Z(λ):

klDivPmf Q (gibbsPmf f λ) = -H(Q) - ⟨λ, 𝔼_Q[f]⟩ + log Z(λ).

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.entropy_le_gibbs_of_constraints

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (c : Fin k → ℝ) (P : α → ℝ) (hP : P ∈ stdSimplex ℝ α) (hP_constraints : ∀ (i : Fin k), ∑ x : α, P x * f i x = c i) (lam : Fin k → ℝ) (h_gibbs_constraints : ∀ (i : Fin k), ∑ x : α, gibbsPmf f lam x * f i x = c i) :

∑ x : α, (P x).negMulLog ≤ ∑ x : α, (gibbsPmf f lam x).negMulLog

Maximum entropy theorem (upper bound, pmf form): under moment constraints ∑ x, P x · f i x = c i for all i, and assuming the same constraints hold for the Boltzmann–Gibbs ansatz gibbsPmf f λ for some fixed Lagrange parameter lam : Fin k → ℝ, the entropy of P is bounded by the entropy of the gibbs distribution:

H(P) ≤ H(gibbsPmf f λ).

The Lagrange parameter lam is passed in as a hypothesis (with the matching constraint witness h_gibbs_constraints), so the result does not need ψ(λ) convexity or any Lagrange-multiplier existence theory.

Used by

Uniqueness #

theorem

InformationTheory.Shannon.MaxEntropyConstrained.klDivPmf_eq_zero_iff_pmf

{α : Type u_1} [Fintype α] {P Q : α → ℝ} (hP : P ∈ stdSimplex ℝ α) (_hQ : Q ∈ stdSimplex ℝ α) (hQ_pos : ∀ (a : α), 0 < Q a) :

CsiszarProjection.klDivPmf P Q = 0 ↔ P = Q

For a full-support reference pmf Q, klDivPmf P Q = 0 ↔ P = Q.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.entropy_eq_gibbs_iff_of_constraints

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (f : Fin k → α → ℝ) (c : Fin k → ℝ) (P : α → ℝ) (hP : P ∈ stdSimplex ℝ α) (hP_constraints : ∀ (i : Fin k), ∑ x : α, P x * f i x = c i) (lam : Fin k → ℝ) (h_gibbs_constraints : ∀ (i : Fin k), ∑ x : α, gibbsPmf f lam x * f i x = c i) :

∑ x : α, (P x).negMulLog = ∑ x : α, (gibbsPmf f lam x).negMulLog ↔ P = gibbsPmf f lam

Maximum entropy theorem (uniqueness, pmf form): H(P) = H(gibbsPmf f λ) if and only if P = gibbsPmf f λ pointwise.

Used by

Special cases #

Zero feature map reduces to uniform pmf #

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsZ_zero

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (lam : Fin k → ℝ) :

gibbsZ 0 lam = ↑(Fintype.card α)

gibbsZ of the zero feature map is just Fintype.card α (each exp 0 = 1 summed N times).

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_zero_eq_uniform

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (lam : Fin k → ℝ) :

gibbsPmf 0 lam = fun (x : α) => 1 / ↑(Fintype.card α)

With the zero feature map, gibbsPmf is the uniform pmf x ↦ 1 / Fintype.card α.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.entropy_uniform_pmf

{α : Type u_1} [Fintype α] [Nonempty α] :

∑ _x : α, (1 / ↑(Fintype.card α)).negMulLog = Real.log ↑(Fintype.card α)

Entropy of the uniform pmf x ↦ 1 / N is log N.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.entropy_gibbsPmf_zero_eq_log_card

{α : Type u_1} [Fintype α] {k : ℕ} [Nonempty α] (lam : Fin k → ℝ) :

∑ x : α, (gibbsPmf 0 lam x).negMulLog = Real.log ↑(Fintype.card α)

With the zero feature map, the Gibbs entropy equals log (Fintype.card α).

Used by

Bernoulli case #

noncomputable def

InformationTheory.Shannon.MaxEntropyConstrained.boolFeature

:

Fin 1 → Bool → ℝ

The two-point feature map: indicator of true.

Equations

InformationTheory.Shannon.MaxEntropyConstrained.boolFeature x✝ b = if b = true then 1 else 0

Instances For

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_bool_sum_eq_one

(lam : Fin 1 → ℝ) :

gibbsPmf boolFeature lam true + gibbsPmf boolFeature lam false = 1

For any λ : Fin 1 → ℝ, gibbsPmf boolFeature λ true + gibbsPmf boolFeature λ false = 1.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_bool_true_eq_of_mean

(lam : Fin 1 → ℝ) (μ : ℝ) (h_mean : ∑ b : Bool, gibbsPmf boolFeature lam b * boolFeature 0 b = μ) :

gibbsPmf boolFeature lam true = μ

For any λ and any μ ∈ (0,1), if the mean constraint gibbsPmf boolFeature λ · 1 + gibbsPmf boolFeature λ · 0 = μ holds, then gibbsPmf boolFeature λ true = μ.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_bool_false_eq_of_mean

(lam : Fin 1 → ℝ) (μ : ℝ) (h_mean : ∑ b : Bool, gibbsPmf boolFeature lam b * boolFeature 0 b = μ) :

gibbsPmf boolFeature lam false = 1 - μ

Under the same mean constraint, gibbsPmf boolFeature λ false = 1 - μ.

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.entropy_gibbsPmf_bool_eq_binEntropy

(lam : Fin 1 → ℝ) (μ : ℝ) (h_mean : ∑ b : Bool, gibbsPmf boolFeature lam b * boolFeature 0 b = μ) :

∑ b : Bool, (gibbsPmf boolFeature lam b).negMulLog = Real.binEntropy μ

Under mean constraint μ, the Gibbs entropy on Bool is exactly the binary entropy Real.binEntropy μ (= textbook -μ log μ - (1-μ) log (1-μ), Ex. 12.1).

Used by

Discretized exponential (geometric ratio form) #

noncomputable def

InformationTheory.Shannon.MaxEntropyConstrained.linearFeature

{N : ℕ} :

Fin 1 → Fin (N + 1) → ℝ

The discrete "linear" feature map on Fin (N+1): f 0 x := (x.val : ℝ).

Equations

InformationTheory.Shannon.MaxEntropyConstrained.linearFeature x✝ x = ↑↑x

Instances For

Used by

theorem

InformationTheory.Shannon.MaxEntropyConstrained.gibbsPmf_linearFeature_eq_geometric

{N : ℕ} (lam : Fin 1 → ℝ) :

gibbsPmf linearFeature lam = fun (x : Fin (N + 1)) => Real.exp (lam 0) ^ ↑x / ∑ y : Fin (N + 1), Real.exp (lam 0) ^ ↑y

Geometric ratio form — setting q := exp (λ 0), the Gibbs distribution with the linear feature is the geometric ratio x ↦ q^x.val / ∑ y, q^y.val on Fin (N+1). Lagrange parameter λ is left as an ansatz; choosing λ 0 = log q then yields the geometric distribution with ratio q.

Used by