Spend your formalization effort on the new mathematics. LeanInfoTheory supplies reusable information-theoretic foundations for research projects and downstream software.
Start with a dependency, not a copy
Create a separate Lean project and depend on v0.1.0 through Lake. Keep the resolved manifest and toolchain under version control. A later library upgrade should be deliberate, followed by a full build of your own project.
Map paper statements to existing results
- List the paper's definitions, theorem statements, and assumptions. Distinguish the target manuscript from supplementary proof sources.
- Match basic identities and inequalities to the theorem highlights and release API, then verify candidate names in a compiling Lean file.
- Keep paper-specific structures and constructions in your project. Propose a library addition when a missing result is independently useful.
- Build one coherent theorem step at a time, including concrete and degenerate examples. Independently review statements as well as proof completion.
Check the mathematical contract
- Alphabet scope: the release targets finite discrete information theory, not general continuous entropy.
- Units: canonical quantities use nats; convert explicitly if the paper uses bits.
- Support: distinguish global assumptions from properties needed only on positive-probability events.
- Conditioning: track argument order and null fibers; a total conditional law's fallback is not evidence about a probability-zero event.
- KL: keep infinity and real-valued conversion separate.
What the release provides
Entropy and information identities, finite-family algebra, independence and Markov characterizations, stochastic data processing, finite Fano inequalities, convexity, and sufficiency are available now. Capacity, AEP, coding theorems, and a dedicated finite-PMF total-variation/coupling API are outside v0.1.0.
Applications and collaboration
A paper formalization and an entropy-inequality certificate application are natural downstream uses. They are not part of this release, and this guide does not claim a completed public case study. Public case studies can be linked here when their authors are ready to publish them.
For a missing theorem, confusing name, or import problem, open an issue with the library version, intended mathematical statement, relevant source section, and a minimal Lean example when possible.