This blueprint mixes implemented modules with planned layers. The
module-level dependency map is
generated from Lean import lines. A source-derived inventory
and the separate signature-bearing v0.1.0 API
reference are available under documentation. Theorem-level
blueprint pages and a blueprint PDF remain future work.
Layer 0: Existing foundations
- mathlib binary and q-ary entropy
- mathlib KL divergence and KL chain-rule infrastructure
- mathlib PMFs, finite measures, Markov kernels, and coding foundations
- PFR-style entropy and mutual-information infrastructure to audit
Layer 1: Finite information measures
- finite random variables and mathlib
PMFs - finite Shannon entropy in nats via
Real.negMulLog, with opt-in scalar conversion to other logarithm bases and bits - entropy invariance under equivalence, injective alphabet relabeling, swaps, and reassociation
- finite entropy upper bound by
log |alphabet|and the uniform-law equality case - joint entropy, conditional entropy, mutual information, and conditional mutual information
- dependent finite-family laws, finite-atom entropy/MI/CMI, pair/triple compatibility, and binary/ordered entropy, MI, and conditional-MI chain rules
- finite-selector PMF mixtures and entropy concavity, including the binary interior-weight equality case
- zero-safe finite log-sum inequality and active-ratio equality with guarded Real corollaries
- finite-selector KL joint convexity, binary KL equality, and mutual-information input-law concavity and channel convexity
- common-base channel conditional KL with finite weighted semantics, a joint KL chain rule, and support-guarded Real forms
- finite-atom mutual independence with restriction/pair laws and n-way entropy-additivity equality characterizations
- marginal mass formulas, support/domination lemmas, and coordinate-orientation lemmas
- semantic bridge theorem identifying entropy with expected self-information over
PMF.toMeasure - finite conditional laws with explicit zero-mass conventions
- conditional entropy as expected entropy of conditional fibers
- mutual information as KL divergence from the joint law to the product of marginals
- conditional mutual information as averaged fiber mutual information and averaged fiber KL
- semantic nonnegativity of mutual information and conditional mutual information
- first mutual-information chain rule
I(A;B,C) = I(A;C) + I(A;B|C)
Layer 2: Semantic bridges and finite theorems
- finite conditional laws and expected-fiber formulas
- KL interpretations and support-aware equality theorems
- independence, conditional independence, and Markov characterizations
- finite stochastic-channel data processing and sufficiency
- finite-family Shannon inequalities and mutual independence
- finite Fano, log-sum, entropy concavity, and KL-convexity results
Layer 3: Documentation and downstream use
- focused public imports, a lightweight mathematical root, and the complete import-only
LeanInfoTheory.Shannonumbrella - source-derived module and declaration references
- versioned signature-bearing API documentation and future theorem-level blueprint pages
- downstream applications built against tagged releases
Layer 4: Network information theory
- future data-processing examples
- future network-converse examples that consume the current finite Fano API
- future cut-set and multi-terminal converse examples