LeanInfoTheory builds on mathlib's probability and analysis foundations to provide a dedicated library for finite Shannon information theory. It is a companion library, not a replacement for mathlib.
Shared probability foundations
Laws are mathlib PMFs. Random-variable distributions use PMF.map, stochastic channels use PMF.bind, and canonical relative entropy uses mathlib's measure-theoretic InformationTheory.klDiv. This shared vocabulary lets proofs reuse the surrounding Lean ecosystem.
A coherent finite-information-theory API
LeanInfoTheory adds finite-PMF entropy and information measures, conditional-law and KL interpretations, textbook identities and inequalities, finite channels and Markov structure, finite-family results, and sufficient-statistic characterizations. The library also connects Boolean-PMF entropy to mathlib's binary entropy.
The theorem map provides mathematical entry points. The v0.1.0 reference contains all 601 supported project-owned declarations, with exact signatures and source links. Imported dependency pages are navigable reference material, not extra LeanInfoTheory declarations.
Imports matched to your proof
The lightweight LeanInfoTheory root exposes core PMF and elementary information-measure APIs. Heavier semantic, KL, channel, and finite-family results are opt-in. Use LeanInfoTheory.Shannon for the complete supported stack, or a focused module for a more targeted dependency.
Version and trust boundaries
LeanInfoTheory v0.1.0 is pinned to Lean and mathlib v4.33.1. The release rejects proof placeholders and audits project proof dependencies, allowing the standard Lean axioms propext, Classical.choice, and Quot.sound. Machine checking establishes a formal consequence of the stated assumptions; it does not by itself establish that a statement captures a paper's intended meaning.
See installation, notation and conventions, and the research-project guide.