Shannon.Entropy.Gibbs

Gibbs inequality and single-variable entropy bounds.

The Gibbs inequality (∑ pᵢ log(qᵢ/pᵢ) ≤ 0) is the analytical workhorse for deriving the properties of Shannon entropy listed in Section 6 of Shannon (1948). It follows from log x ≤ x - 1 and the fact that probability masses sum to one.

We also connect entropyNat to Mathlib's Real.negMulLog, giving access to Mathlib's concavity infrastructure for later proofs.

Main results

• entropyNat_eq_sum_negMulLog: bridge between entropyNat and Real.negMulLog
• gibbs_inequality: ∑ pᵢ log(qᵢ/pᵢ) ≤ 0
• entropyNat_nonneg: H(p) ≥ 0
• entropyNat_uniformPNat: H(uniform n) = log n
• entropyNat_le_log_card: H(p) ≤ log |α|

Bridge to negMulLog

theorem LeanPool.Shannon1948Formalization.entropyNat_eq_sum_negMulLog {α : Type} [Fintype α] (p : ProbDist α) : entropyNat p = ∑ a : α, (↑p a).negMulLog

entropyNat p = ∑ a, negMulLog (p a), connecting our definition to Mathlib's Real.negMulLog which carries concavity and differentiability lemmas.

Gibbs inequality

theorem LeanPool.Shannon1948Formalization.gibbs_inequality {α : Type} [Fintype α] (p q : ProbDist α) (hsupp : ∀ (a : α), 0 < ↑p a → 0 < ↑q a) : ∑ a : α, ↑p a * Real.log (↑q a / ↑p a) ≤ 0

Gibbs inequality: for probability distributions p and q where q covers the support of p, we have ∑ pᵢ log(qᵢ/pᵢ) ≤ 0. Equivalently, the Kullback-Leibler divergence D(p ‖ q) ≥ 0.

The proof uses log x ≤ x - 1 on each ratio qᵢ/pᵢ, then telescopes via ∑ qᵢ = ∑ pᵢ = 1.

Single-variable entropy bounds

theorem LeanPool.Shannon1948Formalization.entropyNat_nonneg {α : Type} [Fintype α] (p : ProbDist α) : 0 ≤ entropyNat p

Entropy is nonnegative: each negMulLog(pᵢ) ≥ 0 for pᵢ ∈ [0, 1].

theorem LeanPool.Shannon1948Formalization.entropyNat_uniformPNat (n : ℕ+) : entropyNat (uniformPNat n) = Real.log ↑↑n

Entropy of the uniform distribution on n outcomes equals log n.

theorem LeanPool.Shannon1948Formalization.entropyNat_le_log_card {α : Type} [Fintype α] [Nonempty α] (p : ProbDist α) : entropyNat p ≤ Real.log ↑(Fintype.card α)

Entropy is at most log |α|, with equality at the uniform distribution. The proof applies gibbs_inequality with q = uniform.