Module Guide

This hand-written import guide complements the signature-bearing v0.1.0 API reference and the supplementary source-derived declaration inventory. The versioned API tree is generated from the exact release commit and served at the stable route above.

Import LeanInfoTheory for the lightweight mathematical API, LeanInfoTheory.Shannon for the complete supported mathematical stack, or a focused module when dependency weight matters. Basic, Examples, and MathlibFragments are non-stable anchors excluded from both mathematical umbrellas.

• LeanInfoTheory.Basic: non-stable development anchor for project metadata and roadmap vocabulary.
• LeanInfoTheory.Probability.Finite: real-mass, finite-bind, support, and pointwise PMF.map bridge lemmas.
• LeanInfoTheory.Probability.FiniteChannel: opt-in, type-generic PMF-valued channel constructions and their atom, projection, composition, deterministic-map, and support laws.
• LeanInfoTheory.Probability.FiniteMixture: opt-in binary PMF mixtures with NNReal weights and exact endpoint laws; general selectors use PMF.bind.
• LeanInfoTheory.Shannon: import-only umbrella for the complete supported mathematical stack.
• LeanInfoTheory.Shannon.Entropy: finite Shannon entropy, random-variable entropy, zero-entropy characterizations, and relabeling invariance theorems.
• LeanInfoTheory.Shannon.EntropyBounds: Jensen-based alphabet and support-cardinality upper bounds plus the uniform-law equality theorem. Import this module explicitly when those heavier analytic bounds are needed.
• LeanInfoTheory.Shannon.EntropyConcavity: opt-in finite-selector entropy concavity with a binary textbook corollary and interior-weight equality characterization.
• LeanInfoTheory.Shannon.BinaryEntropy: opt-in Boolean-PMF bridge identifying local entropy with mathlib's Real.binEntropy.
• LeanInfoTheory.Shannon.Fano: opt-in deterministic-decoder error API, exact and q-ary finite Fano inequalities, weak forms, random-variable wrappers, and converse-facing corollaries.
• LeanInfoTheory.Shannon.FiniteFamily: opt-in dependent finite-family laws, finite marginals, entropy/MI/CMI algebra, pair/triple compatibility, and binary/ordered entropy, MI, and conditional-MI chain rules.
• LeanInfoTheory.Shannon.InfoMeasures: marginals, conditional entropy, mutual information, conditional mutual information, chain rules, symmetry, and textbook entropy identities.
• LeanInfoTheory.Shannon.LogSum: opt-in zero-safe finite EReal log-sum inequality and equality characterization with guarded Real corollaries.
• LeanInfoTheory.Shannon.Units: lightweight opt-in scalar conversion from canonical nats to arbitrary valid logarithm bases, with base 2 named for bits. It remains outside the lightweight root and does not duplicate the information-measure hierarchy.
• LeanInfoTheory.Shannon.SemanticBridge: import-only bridge entry point for expected self-information, finite conditional laws, KL and conditional-KL formulas, convexity, independence, Markov and sufficiency semantics, recovery, stochastic data processing, pair/triple inequalities, and finite-family semantics.
• LeanInfoTheory.Shannon.SemanticBridge.Entropy: focused owner for self-information and finite entropy as expected self-information.
• LeanInfoTheory.Shannon.SemanticBridge.Product: independent-product PMF infrastructure, product-measure bridge lemmas, and joint-law absolute-continuity facts.
• LeanInfoTheory.Shannon.SemanticBridge.FiniteSums: finite real-sum rewrites for marginals, entropy, and the log-ratio formula for mutual information.
• LeanInfoTheory.Shannon.SemanticBridge.Conditional: finite conditional-law API and expected conditional entropy / conditional mutual information fiber formulas.
• LeanInfoTheory.Shannon.SemanticBridge.ConditionalKL: common-base channel conditional KL, finite weighted semantics, the joint KL chain rule, and support-guarded Real forms.
• LeanInfoTheory.Shannon.SemanticBridge.Convexity: finite-selector KL joint convexity, binary KL equality, and mutual-information input-law concavity and channel convexity.
• LeanInfoTheory.Shannon.SemanticBridge.FiniteFamily: finite-family monotonicity, nonnegativity, submodularity, MI bounds, conditioning reduction, and binary/n-way subadditivity.
• LeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependence: finite-atom PMF/source mutual independence, restriction and pair laws, and n-way entropy-additivity equality characterizations.
• LeanInfoTheory.Shannon.SemanticBridge.KL: finite KL expansion, mutual information as KL, and averaged conditional-KL bridge theorems.
• LeanInfoTheory.Shannon.SemanticBridge.Independence: ordinary and conditional independence predicates, mathlib bridges, positive-fiber formulations, and zero-MI/zero-CMI characterizations.
• LeanInfoTheory.Shannon.SemanticBridge.Markov: finite Markov predicates and characterizations, total conditional channels, canonical/existential channel factorization, exact information loss, and MI data processing.
• LeanInfoTheory.Shannon.SemanticBridge.Sufficiency: lightweight fixed-prior and model-family sufficiency predicates, information-preservation characterizations, exact full-joint recovery, and finite factorization results.
• LeanInfoTheory.Shannon.SemanticBridge.DataProcessing: PMF-channel-to-kernel and posterior bridges, exact KL decomposition, finite KL contraction, invariant-law consequences, and doubly stochastic entropy growth.
• LeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KL: downstream KL preservation and guarded converse theorems for sufficient channels and deterministic statistics.
• LeanInfoTheory.Shannon.SemanticBridge.Theorems: user-facing semantic theorems, including nonnegativity, zero conditional entropy, deterministic entropy/MI processing, chain-rule variants, and ordinary/conditional inequality bands.
• LeanInfoTheory.InformationMeasures: public convenience re-export for the finite information-measure API; theorem-oriented code should usually prefer the canonical LeanInfoTheory.Shannon names.
• LeanInfoTheory.Examples.SupportSensitive: opt-in support-cardinality, conditional-fiber, functional-dependence, and recovery examples.
• LeanInfoTheory.Examples.KLTop: opt-in disjoint-support example demonstrating the need for finiteness guards in real-valued KL equality statements.
• LeanInfoTheory.Examples.CommonCause: opt-in noisy binary common-cause example exercising conditional independence, zero CMI, and Markov factorization.
• LeanInfoTheory.Examples.ConditionalKL: opt-in private regression consumers for null, active, finite, infinite, and support-guarded common-base conditional KL.
• LeanInfoTheory.Examples.StochasticChannels: opt-in stochastic reset/cascade examples exercising KL contraction, support-sensitive real bounds, and strict entropy growth.
• LeanInfoTheory.Examples.SufficientStatistics: opt-in fixed-prior and family-sufficiency examples covering recovery, factorization, KL preservation, and failure modes.
• LeanInfoTheory.Examples.Convexity: opt-in private regression consumers for scalar log-sum, finite mixtures, entropy concavity, KL convexity, and MI input-law concavity and channel convexity.
• LeanInfoTheory.Examples.Fano: opt-in examples covering perfect decoding, the singleton-source edge case, and a fair Boolean source with a constant observation.
• LeanInfoTheory.Examples.FiniteFamily: opt-in homogeneous and dependent-alphabet examples exercising ordered entropy/MI/CMI chains, overlap, empty entropy, product laws, and pairwise-but-not-mutual independence.
• LeanInfoTheory.Examples.Units: opt-in maintained consumers for arbitrary-base, bits, entropy, MI, CMI, and finiteness-guarded real-KL conversion.
• LeanInfoTheory.Examples: non-stable aggregate for all maintained regression consumers, including information-unit conversions.
• LeanInfoTheory.MathlibFragments: non-stable reference anchor for heavier mathlib information-theory and coding imports.

Human-facing design notes are tracked in docs/foundation-conventions.md and docs/project-log.md in the repository.