SamuelSchlesingershannon-entropy0.1.0

A formalization of Shannon's seminal 1948 paper defining entropy.

Shannon Entropy Characterization in Lean

Lean License: MIT

This repository formalizes Shannon's finite-alphabet characterization theorem from Shannon (1948), Appendix 2.

The central result is:

  • For any uncertainty functional H satisfying the Shannon-style axiom bundle (continuity, strict monotonicity on uniform distributions, grouping, and relabel invariance), there is a positive constant K such that H(p) = -K * Σ p_i log p_i.
  • Equivalently, for any base b > 1, there is Kb > 0 such that H(p) = -Kb * Σ p_i log_b p_i.

Formalization Scope

  • Finite alphabets only.
  • Real-valued probability vectors with explicit simplex proofs.
  • Proof structure follows Shannon's Appendix-2 phases:
    1. Equiprobable case (A(n) behaves logarithmically).
    2. Rational probabilities via grouped equiprobable refinement.
    3. Extension to real probabilities via continuity and rational approximation.

Main Theorems

Characterization (Appendix 2)

  • entropyNat_unique: Shannon/Entropy/Final.lean
  • entropyBase_unique: Shannon/Entropy/Final.lean

Converse

  • entropyNat_shannonAxioms: entropyNat satisfies ShannonEntropyAxioms — Shannon/Entropy/Converse.lean

Section 6 Properties

  • entropyNat_eq_zero_iff: H = 0 iff deterministic — Shannon/Entropy/Properties.lean
  • entropyNat_eq_log_card_iff: H = log|α| iff uniform — Shannon/Entropy/Properties.lean
  • entropyNat_joint_le_add: subadditivity H(X,Y) ≤ H(X) + H(Y) — Shannon/Entropy/Properties.lean
  • entropyNat_doublyStochastic_le: Schur-concavity H(Ap) ≥ H(p) — Shannon/Entropy/Properties.lean
  • condEntropy_le_entropyNat: conditioning reduces entropy — Shannon/Entropy/Properties.lean
  • condEntropy_nonneg: conditional entropy ≥ 0 — Shannon/Entropy/Properties.lean
  • chain_rule: H(X,Y) = H(X) + H_X(Y) — Shannon/Entropy/Joint.lean
  • entropyNat_prodDist: H(X×Y) = H(X) + H(Y) — Shannon/Entropy/Joint.lean

Module Layout

  • Shannon/Entropy/Core.lean Foundations: probability distributions, axiom bundle, core constructions.
  • Shannon/Entropy/Uniform.lean Phase 1: equiprobable characterization.
  • Shannon/Entropy/Rational.lean Phase 2: rational case + worked (1/2, 1/3, 1/6) grouping example.
  • Shannon/Entropy/Approx.lean Phase 3: floor-count rational approximants and convergence lemmas.
  • Shannon/Entropy/Final.lean Final uniqueness theorems.
  • Shannon/Entropy/Gibbs.lean Gibbs inequality, negMulLog bridge, entropy nonnegativity, uniform entropy.
  • Shannon/Entropy/Joint.lean Joint distributions, marginals, conditional entropy, chain rule.
  • Shannon/Entropy/Properties.lean Section 6 properties: deterministic iff, uniform iff, subadditivity, Schur-concavity, conditioning.
  • Shannon/Entropy/Converse.lean Converse: entropyNat satisfies the Shannon axioms, completing the iff characterization.
  • Shannon/Entropy.lean Facade import.
  • Shannon.lean Project entrypoint.

How To Read The Proof

If you want to read this like a paper:

  1. Start in Shannon/Entropy/Core.lean for definitions and axioms.
  2. Read Shannon/Entropy/Uniform.lean for the equiprobable logarithm law (Apos H n = K * log n).
  3. Read Shannon/Entropy/Rational.lean for rational distributions via grouping.
  4. Read Shannon/Entropy/Approx.lean for the continuity bridge (approxProb p N → p).
  5. Finish in Shannon/Entropy/Final.lean for the final uniqueness theorems.
  6. Continue to Shannon/Entropy/Gibbs.lean for the Gibbs inequality.
  7. Read Shannon/Entropy/Joint.lean for joint distributions and the chain rule.
  8. Read Shannon/Entropy/Properties.lean for the Section 6 entropy properties.
  9. Read Shannon/Entropy/Converse.lean for the proof that entropyNat satisfies the axioms.

For pedagogical context, see the worked decomposition theorem in Shannon/Entropy/Rational.lean:

  • worked_grouping_identity
  • workedCompose_masses

Build and Verify

Requirements:

  • Lean toolchain from lean-toolchain
  • Lake (bundled with Lean)

Commands:

lake build

CI workflow:

  • .github/workflows/lean_action_ci.yml (Lean Action CI)

Notes on Axioms

Shannon's symmetry principle ("depends only on probabilities, not labels") is represented explicitly as:

  • ShannonEntropyAxioms.relabelInvariant

This makes permutation/relabeling steps fully explicit in Lean proofs.

AI Assistance

This project was developed with substantial assistance from Claude (Anthropic). Claude contributed to proof development, code structure, and documentation throughout the formalization effort.

Reference

  • Claude E. Shannon, A Mathematical Theory of Communication (1948). The repository includes shannon1948.pdf for study context.

License

This project is licensed under the MIT License. See LICENSE.