Use familiar information-theoretic quantities directly in Lean proofs. LeanInfoTheory provides both joint-law and random-variable APIs over mathlib probability mass functions.
From textbook notation to the API
All names in this table live in LeanInfoTheory.Shannon. The random variables are functions on a common source carrying the law p; their quantities are defined through pushforward laws.
| Quantity | Lean expression |
|---|---|
| H(X) | entropyOf p X |
| H(X | Y) | condEntropyOf p X Y |
| I(X;Y) | mutualInfoOf p X Y |
| I(X;Y | Z) | condMutualInfoOf p X Y Z |
For a law q directly on the relevant alphabet, use entropy q; on a pair use condEntropy q or mutualInfo q; on a triple use condMutualInfo q. Conditional entropy conditions the first coordinate on the second, and conditional mutual information conditions the first two on the third.
Lean product types are right-associated. In the conditional mutual information API, the last argument is the conditioning variable. Check exact finite-type assumptions in the information-measure reference.
Mutual information is nonnegative
import LeanInfoTheory.Shannon.SemanticBridge.Theorems
open LeanInfoTheory.Shannon
example (p : PMF (Bool × Bool)) : 0 <= mutualInfo p := by
exact mutualInfo_nonneg pThe semantic layer connects the finite definitions to conditional laws and mathlib KL divergence. Elementary definitions and identities remain in the lightweight layer.
Nats and bits
Canonical real-valued information quantities use natural logarithms and are measured in nats. Import LeanInfoTheory.Shannon.Units to use natsToBits, which divides by Real.log 2. The units API also supports other valid bases; their information-theoretic interpretation requires a base greater than one.
KL divergence can be infinite
The canonical KL divergence is mathlib's InformationTheory.klDiv p.toMeasure q.toMeasure, valued in ENNReal. The finite-PMF bridge relates support, finiteness, and equality. Establish the theorem's support or finiteness hypothesis before converting KL to Real: Lean's total conversion sends infinity to zero, which is not a finite divergence interpretation.
Mathematical sources
Cover and Thomas, Elements of Information Theory (1991), Chapter 2, especially Sections 2.1-2.6. This guide explains the library's finite-discrete contracts, not a verbatim transcription of the textbook. See also the relationship with mathlib.