Latest stable release: v0.1.0, the first LeanInfoTheory
public-library baseline, archived as
10.5281/zenodo.22229599.
601 documented public declarations. 31 supported modules.
Ready to use in your own Lean project.
Put machine-checked information theory to work. LeanInfoTheory is a reusable Lean 4 and mathlib library for finite discrete information theory, bringing entropy, mutual information, KL divergence, channels, Markov chains, data processing, Fano inequalities, and sufficient statistics into one substantial mathematical toolkit.
Build research formalizations and information-theoretic software on proved foundations. Install the tagged release, choose a focused import, and reuse the results in your own proofs. Every formal theorem is checked by Lean against its stated assumptions; the maintained release validation rejects proof placeholders.
Install and prove your first result or explore the research-project guide.
Entropy, conditional entropy, mutual information, conditional mutual information, relabeling invariance, and finite entropy upper-bound results are checked in Lean, together with dependent finite-subfamily measures, ordered entropy/MI/CMI chain rules, finite-atom mutual independence, finite mixtures, and entropy concavity.
See theorem highlightsThe finite definitions are connected to expected self-information, conditional laws, KL divergence, independence and Markov characterizations, MI/KL data processing, entropy growth under doubly stochastic channels, KL joint convexity with binary equality, common-base conditional KL and its joint chain rule, and MI input-law concavity and channel convexity.
See bridge statementsFinite channel composition, stochastic data processing, deterministic-decoder Fano bounds, exact recovery, and support-aware sufficiency theorems are available as focused APIs.
See the module guideA signature-bearing v0.1.0 reference covers all 31 supported modules and 601 supported declarations. The generated reference also carries the complete imported dependency closure for working links and search. The source-derived inventory and module-level dependency map remain separate supplementary artifacts.
Proved foundation
Entropy, conditional entropy, mutual information, conditional
mutual information, marginal APIs, entropy bounds, relabeling,
swaps, reassociation, dependent-family CMI chains and mutual
independence, finite PMF mixtures, log-sum, and entropy concavity
over mathlib PMFs.
Proved bridge
Entropy as expected self-information, finite conditional laws, mutual information as KL, independence and Markov equivalences, averaged conditional-KL, stochastic MI/KL data processing, and invariant-law, entropy-growth, and finite-family Shannon inequalities, KL joint convexity/equality, common-base conditional KL, finite-family mutual-independence equality, and MI input-law concavity and channel convexity.
Proved structure
Type-generic PMF channels, channel composition and support laws, Markov factorization, KL and mutual-information data processing, sufficient statistics, and common recovery.
Proved extensions
Sharp finite entropy bounds, Fano inequalities, zero-safe log-sum, entropy concavity, KL convexity, and equality cases.
Formal library branch
Focused extension modules
A lightweight root exposes the core mathematical API, while heavier analytic, KL, channel, finite-family, and example layers remain explicitly importable.
Later milestones extend the reusable theorem surface and generated documentation without pulling application-specific constructions into the library root.
| Mathematical statement | Lean theorem | Status |
|---|---|---|
H(P) >= 0 |
Shannon.entropy_nonneg |
Proved |
H(P) <= log |alpha| |
Shannon.entropy_le_log_card |
Proved |
I(A;B) = D(P_AB || P_A x P_B) |
Shannon.mutualInfo_eq_toReal_klDiv_joint_indepProd |
Proved |
0 <= I(A;B) and 0 <= I(A;B | C) |
Shannon.mutualInfo_nonneg, Shannon.condMutualInfo_nonneg |
Proved |
| Finite-family entropy is submodular | Shannon.familyEntropy_submodular |
Proved |
| Finite deterministic-decoder Fano inequality | Shannon.condEntropy_fano |
Proved |
| KL divergence contracts through a finite channel | Shannon.klDiv_channel_le |
Proved |
| Entropy additivity characterizes finite-family mutual independence | Shannon.familyEntropy_eq_sum_singletons_iff_isMutuallyIndependentFamily |
Proved |
Release declarations are checked by Lean's kernel and the maintained project builds. Continuous integration also regenerates the source-derived references and rejects proof placeholders in project Lean source.
Kernel checking establishes that formal declarations follow from their formal assumptions; theorem selection, assumptions, conventions, and mathematical interpretation remain human responsibilities.
ec78829 after passing the full milestone validation suite.7b5f0db.C7.22. The coherent Lean/source checkpoint is commit 5e616d8.C8.24. Its focused, maintained, and default builds, consumers, trust audit, generated references, website checks, and repository hygiene pass. The validated source is checkpointed as 1eef228; its required Lean build/placeholder and Pages workflows both succeeded.