Generated by scripts/generate_website_blueprint.py from
local Lean import lines. This remains a module-level map,
not a theorem-level leanblueprint graph. The separate
v0.1.0 API route is populated from
signature-bearing doc-gen output during website assembly.
Current Graph
46local modules
94local import edges
5root-reachable modules
41separate-import modules
Layer Summary
| Layer | Modules | Root reachable | Separate import |
|---|---|---|---|
| Root import | 1 | 1 | 0 |
| Shared foundation | 3 | 1 | 2 |
| Finite Shannon layer | 11 | 3 | 8 |
| Semantic bridge layer | 16 | 0 | 16 |
| Non-stable anchors | 15 | 0 | 15 |
Module Inventory
| Module | Layer | Import surface | Summary | Source file |
|---|---|---|---|---|
LeanInfoTheory | Root import | root | Lightweight public root import for finite PMF and Shannon APIs. | LeanInfoTheory.lean |
LeanInfoTheory.Probability.Finite | Shared foundation | root reachable | Finite PMF real-mass, finite-bind, support, and pointwise PMF.map bridge lemmas. | LeanInfoTheory/Probability/Finite.lean |
LeanInfoTheory.Probability.FiniteChannel | Shared foundation | separate import | Type-generic PMF channel constructions and their elementary laws. | LeanInfoTheory/Probability/FiniteChannel.lean |
LeanInfoTheory.Probability.FiniteMixture | Shared foundation | separate import | Binary PMF mixtures with NNReal weights and exact endpoint laws; general finite selectors use PMF.bind. | LeanInfoTheory/Probability/FiniteMixture.lean |
LeanInfoTheory.InformationMeasures | Finite Shannon layer | root reachable | Convenience re-export for the finite information-measure API. | LeanInfoTheory/InformationMeasures.lean |
LeanInfoTheory.Shannon | Finite Shannon layer | separate import | Import-only umbrella for the complete supported finite information-theory stack. | LeanInfoTheory/Shannon.lean |
LeanInfoTheory.Shannon.BinaryEntropy | Finite Shannon layer | separate import | Boolean-PMF entropy bridge to mathlib's Real.binEntropy. | LeanInfoTheory/Shannon/BinaryEntropy.lean |
LeanInfoTheory.Shannon.Entropy | Finite Shannon layer | root reachable | Finite Shannon entropy, entropy of finite-valued random variables, and first entropy invariance theorems. | LeanInfoTheory/Shannon/Entropy.lean |
LeanInfoTheory.Shannon.EntropyBounds | Finite Shannon layer | separate import | Sharp alphabet/support entropy bounds and their uniform-law equality cases. | LeanInfoTheory/Shannon/EntropyBounds.lean |
LeanInfoTheory.Shannon.EntropyConcavity | Finite Shannon layer | separate import | Finite-selector entropy concavity and its binary interior-weight equality characterization, proved directly by Jensen. | LeanInfoTheory/Shannon/EntropyConcavity.lean |
LeanInfoTheory.Shannon.Fano | Finite Shannon layer | separate import | Deterministic decoding error, exact and weak finite Fano inequalities, and converse-facing corollaries. | LeanInfoTheory/Shannon/Fano.lean |
LeanInfoTheory.Shannon.FiniteFamily | Finite Shannon layer | separate import | Dependent finite-family laws, finite marginals, family entropy/MI/CMI algebra, pair/triple bridges, and binary/ordered entropy, MI, and conditional-MI chain rules. | LeanInfoTheory/Shannon/FiniteFamily.lean |
LeanInfoTheory.Shannon.InfoMeasures | Finite Shannon layer | root reachable | Marginals, conditional entropy, mutual information, conditional mutual information, orientation lemmas, and the auxiliary-variable information decomposition. | LeanInfoTheory/Shannon/InfoMeasures.lean |
LeanInfoTheory.Shannon.LogSum | Finite Shannon layer | separate import | Zero-safe finite EReal log-sum inequality and equality with guarded Real corollaries. | LeanInfoTheory/Shannon/LogSum.lean |
LeanInfoTheory.Shannon.Units | Finite Shannon layer | separate import | Opt-in scalar conversion from canonical nats to arbitrary valid logarithm bases and bits. | LeanInfoTheory/Shannon/Units.lean |
LeanInfoTheory.Shannon.SemanticBridge | Semantic bridge layer | separate import | Import-only aggregate for finite semantic, KL, convexity, conditional-KL, independence, Markov, sufficiency, data-processing, recovery, and finite-family bridges. | LeanInfoTheory/Shannon/SemanticBridge.lean |
LeanInfoTheory.Shannon.SemanticBridge.Conditional | Semantic bridge layer | separate import | Finite conditional-law API and expected conditional entropy / conditional mutual-information formulas. | LeanInfoTheory/Shannon/SemanticBridge/Conditional.lean |
LeanInfoTheory.Shannon.SemanticBridge.ConditionalKL | Semantic bridge layer | separate import | Common-base channel conditional KL, finite weighted semantics, joint KL chain rule, and support-guarded Real forms. | LeanInfoTheory/Shannon/SemanticBridge/ConditionalKL.lean |
LeanInfoTheory.Shannon.SemanticBridge.Convexity | Semantic bridge layer | separate import | Finite-selector KL joint convexity, binary KL equality, and mutual-information input-law concavity and channel convexity. | LeanInfoTheory/Shannon/SemanticBridge/Convexity.lean |
LeanInfoTheory.Shannon.SemanticBridge.DataProcessing | Semantic bridge layer | separate import | Finite channel posteriors, supported sufficiency, KL data processing and equality, and entropy-growth consequences. | LeanInfoTheory/Shannon/SemanticBridge/DataProcessing.lean |
LeanInfoTheory.Shannon.SemanticBridge.Entropy | Semantic bridge layer | separate import | Expected-self-information semantics for finite entropy. | LeanInfoTheory/Shannon/SemanticBridge/Entropy.lean |
LeanInfoTheory.Shannon.SemanticBridge.FiniteFamily | Semantic bridge layer | separate import | Finite-family Shannon inequalities, including submodularity and n-way subadditivity. | LeanInfoTheory/Shannon/SemanticBridge/FiniteFamily.lean |
LeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependence | Semantic bridge layer | separate import | Dependent-family mutual independence, restriction and pair laws, and n-way entropy-additivity equality characterizations. | LeanInfoTheory/Shannon/SemanticBridge/FiniteFamilyIndependence.lean |
LeanInfoTheory.Shannon.SemanticBridge.FiniteSums | Semantic bridge layer | separate import | Finite real-sum rewrites and mutual-information log-ratio formulas. | LeanInfoTheory/Shannon/SemanticBridge/FiniteSums.lean |
LeanInfoTheory.Shannon.SemanticBridge.Independence | Semantic bridge layer | separate import | PMF-first ordinary/conditional independence, arbitrary-type deterministic postprocessing, zero MI/CMI, and entropy equality cases. | LeanInfoTheory/Shannon/SemanticBridge/Independence.lean |
LeanInfoTheory.Shannon.SemanticBridge.KL | Semantic bridge layer | separate import | PMF support/KL finiteness and equality, uniform-reference identities, and MI/CMI KL bridges. | LeanInfoTheory/Shannon/SemanticBridge/KL.lean |
LeanInfoTheory.Shannon.SemanticBridge.Markov | Semantic bridge layer | separate import | Finite Markov characterizations, channel factorization, information loss, and mutual-information data processing. | LeanInfoTheory/Shannon/SemanticBridge/Markov.lean |
LeanInfoTheory.Shannon.SemanticBridge.Product | Semantic bridge layer | separate import | Independent-product PMFs, product-measure semantics, support formulas, and absolute-continuity facts. | LeanInfoTheory/Shannon/SemanticBridge/Product.lean |
LeanInfoTheory.Shannon.SemanticBridge.Sufficiency | Semantic bridge layer | separate import | Fixed-prior and model-family sufficiency, common recovery, and full-support/all-prior characterizations. | LeanInfoTheory/Shannon/SemanticBridge/Sufficiency.lean |
LeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KL | Semantic bridge layer | separate import | Pairwise KL preservation and guarded equality characterizations through common exact recovery. | LeanInfoTheory/Shannon/SemanticBridge/Sufficiency/KL.lean |
LeanInfoTheory.Shannon.SemanticBridge.Theorems | Semantic bridge layer | separate import | User-facing semantic nonnegativity, chain rules, deterministic processing, and information inequalities. | LeanInfoTheory/Shannon/SemanticBridge/Theorems.lean |
LeanInfoTheory.Basic | Non-stable anchors | non-stable | Non-stable development anchor for project metadata and roadmap vocabulary. | LeanInfoTheory/Basic.lean |
LeanInfoTheory.Examples | Non-stable anchors | non-stable | Non-stable aggregate for maintained conditional-KL, convexity, finite-family, independence-processing, information-decomposition, support-sensitive, Markov, channel, sufficiency, Fano, and units regression consumers. | LeanInfoTheory/Examples.lean |
LeanInfoTheory.Examples.CommonCause | Non-stable anchors | non-stable | Noisy binary common-cause example for conditional independence and Markov factorization. | LeanInfoTheory/Examples/CommonCause.lean |
LeanInfoTheory.Examples.ConditionalKL | Non-stable anchors | non-stable | Private maintained regressions for common-base conditional KL across null, active, finite, infinite, and guarded Real cases. | LeanInfoTheory/Examples/ConditionalKL.lean |
LeanInfoTheory.Examples.Convexity | Non-stable anchors | non-stable | Private maintained regressions for finite log-sum, mixtures, entropy concavity, KL convexity, and mutual-information input-law concavity and channel convexity. | LeanInfoTheory/Examples/Convexity.lean |
LeanInfoTheory.Examples.Fano | Non-stable anchors | non-stable | Perfect-decoder, singleton-source, and nonzero-error examples for the finite Fano API. | LeanInfoTheory/Examples/Fano.lean |
LeanInfoTheory.Examples.FiniteFamily | Non-stable anchors | non-stable | Homogeneous and dependent-alphabet finite-family examples covering conditional-MI chains, product laws, and pairwise-but-not-mutual independence. | LeanInfoTheory/Examples/FiniteFamily.lean |
LeanInfoTheory.Examples.IndependenceProcessing | Non-stable anchors | non-stable | Private arbitrary-PMF consumers for non-injective and constant independence postprocessing, infinite types, symmetry, and finite zero mutual information. | LeanInfoTheory/Examples/IndependenceProcessing.lean |
LeanInfoTheory.Examples.InformationDecomposition | Non-stable anchors | non-stable | Private lightweight consumers for the auxiliary-variable MI decomposition, algebraic zero terms, singleton variables, and sparse joint laws. | LeanInfoTheory/Examples/InformationDecomposition.lean |
LeanInfoTheory.Examples.KLTop | Non-stable anchors | non-stable | Disjoint-support PMF example exposing the infinite-KL toReal zero trap. | LeanInfoTheory/Examples/KLTop.lean |
LeanInfoTheory.Examples.StochasticChannels | Non-stable anchors | non-stable | Finite stochastic-channel examples for KL contraction, cascade support, and entropy growth. | LeanInfoTheory/Examples/StochasticChannels.lean |
LeanInfoTheory.Examples.SufficientStatistics | Non-stable anchors | non-stable | Finite sufficient-statistics examples covering noninjective sufficiency, constant-statistic failure, and recovery/posterior/KL boundaries. | LeanInfoTheory/Examples/SufficientStatistics.lean |
LeanInfoTheory.Examples.SupportSensitive | Non-stable anchors | non-stable | Support-aware entropy, conditional-fiber, functional-dependence, and recovery examples. | LeanInfoTheory/Examples/SupportSensitive.lean |
LeanInfoTheory.Examples.Units | Non-stable anchors | non-stable | Private maintained regressions for arbitrary-base, bits, entropy, MI, CMI, and guarded real-KL conversion. | LeanInfoTheory/Examples/Units.lean |
LeanInfoTheory.MathlibFragments | Non-stable anchors | non-stable | Non-stable reference checklist of heavier mathlib information-theory and coding anchors. | LeanInfoTheory/MathlibFragments.lean |
Local Import Edges
| Module | Local imports | External imports |
|---|---|---|
LeanInfoTheory | LeanInfoTheory.InformationMeasuresLeanInfoTheory.Probability.Finite | 0 |
LeanInfoTheory.Probability.Finite | none | 4 |
LeanInfoTheory.Probability.FiniteChannel | LeanInfoTheory.Probability.Finite | 0 |
LeanInfoTheory.Probability.FiniteMixture | LeanInfoTheory.Probability.Finite | 0 |
LeanInfoTheory.InformationMeasures | LeanInfoTheory.Shannon.EntropyLeanInfoTheory.Shannon.InfoMeasures | 0 |
LeanInfoTheory.Shannon | LeanInfoTheoryLeanInfoTheory.Shannon.FanoLeanInfoTheory.Shannon.SemanticBridgeLeanInfoTheory.Shannon.Units | 0 |
LeanInfoTheory.Shannon.BinaryEntropy | LeanInfoTheory.Shannon.Entropy | 1 |
LeanInfoTheory.Shannon.Entropy | LeanInfoTheory.Probability.Finite | 2 |
LeanInfoTheory.Shannon.EntropyBounds | LeanInfoTheory.Shannon.Entropy | 2 |
LeanInfoTheory.Shannon.EntropyConcavity | LeanInfoTheory.Probability.FiniteMixtureLeanInfoTheory.Shannon.Entropy | 1 |
LeanInfoTheory.Shannon.Fano | LeanInfoTheory.Shannon.BinaryEntropyLeanInfoTheory.Shannon.EntropyBoundsLeanInfoTheory.Shannon.SemanticBridge.Theorems | 0 |
LeanInfoTheory.Shannon.FiniteFamily | LeanInfoTheory.Shannon.InfoMeasures | 2 |
LeanInfoTheory.Shannon.InfoMeasures | LeanInfoTheory.Shannon.Entropy | 0 |
LeanInfoTheory.Shannon.LogSum | none | 4 |
LeanInfoTheory.Shannon.Units | LeanInfoTheory.Shannon.InfoMeasures | 1 |
LeanInfoTheory.Shannon.SemanticBridge | LeanInfoTheory.Shannon.SemanticBridge.ConditionalLeanInfoTheory.Shannon.SemanticBridge.ConditionalKLLeanInfoTheory.Shannon.SemanticBridge.ConvexityLeanInfoTheory.Shannon.SemanticBridge.DataProcessingLeanInfoTheory.Shannon.SemanticBridge.EntropyLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependenceLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsLeanInfoTheory.Shannon.SemanticBridge.IndependenceLeanInfoTheory.Shannon.SemanticBridge.KLLeanInfoTheory.Shannon.SemanticBridge.MarkovLeanInfoTheory.Shannon.SemanticBridge.ProductLeanInfoTheory.Shannon.SemanticBridge.SufficiencyLeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KLLeanInfoTheory.Shannon.SemanticBridge.Theorems | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Conditional | LeanInfoTheory.Shannon.InfoMeasures | 1 |
LeanInfoTheory.Shannon.SemanticBridge.ConditionalKL | LeanInfoTheory.Shannon.SemanticBridge.DataProcessingLeanInfoTheory.Shannon.SemanticBridge.KL | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Convexity | LeanInfoTheory.Probability.FiniteChannelLeanInfoTheory.Probability.FiniteMixtureLeanInfoTheory.Shannon.EntropyConcavityLeanInfoTheory.Shannon.LogSumLeanInfoTheory.Shannon.SemanticBridge.KLLeanInfoTheory.Shannon.SemanticBridge.Product | 0 |
LeanInfoTheory.Shannon.SemanticBridge.DataProcessing | LeanInfoTheory.Shannon.SemanticBridge.MarkovLeanInfoTheory.Shannon.SemanticBridge.Sufficiency | 2 |
LeanInfoTheory.Shannon.SemanticBridge.Entropy | LeanInfoTheory.Shannon.Entropy | 1 |
LeanInfoTheory.Shannon.SemanticBridge.FiniteFamily | LeanInfoTheory.Shannon.FiniteFamilyLeanInfoTheory.Shannon.SemanticBridge.Theorems | 0 |
LeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependence | LeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyLeanInfoTheory.Shannon.SemanticBridge.Independence | 0 |
LeanInfoTheory.Shannon.SemanticBridge.FiniteSums | LeanInfoTheory.Shannon.InfoMeasures | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Independence | LeanInfoTheory.Shannon.SemanticBridge.Theorems | 1 |
LeanInfoTheory.Shannon.SemanticBridge.KL | LeanInfoTheory.Shannon.SemanticBridge.ConditionalLeanInfoTheory.Shannon.SemanticBridge.FiniteSumsLeanInfoTheory.Shannon.SemanticBridge.Product | 3 |
LeanInfoTheory.Shannon.SemanticBridge.Markov | LeanInfoTheory.Probability.FiniteChannelLeanInfoTheory.Shannon.SemanticBridge.Independence | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Product | LeanInfoTheory.Shannon.InfoMeasures | 2 |
LeanInfoTheory.Shannon.SemanticBridge.Sufficiency | LeanInfoTheory.Shannon.SemanticBridge.Markov | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KL | LeanInfoTheory.Shannon.SemanticBridge.DataProcessing | 0 |
LeanInfoTheory.Shannon.SemanticBridge.Theorems | LeanInfoTheory.Shannon.SemanticBridge.KL | 0 |
LeanInfoTheory.Basic | none | 0 |
LeanInfoTheory.Examples | LeanInfoTheory.Examples.CommonCauseLeanInfoTheory.Examples.ConditionalKLLeanInfoTheory.Examples.ConvexityLeanInfoTheory.Examples.FanoLeanInfoTheory.Examples.FiniteFamilyLeanInfoTheory.Examples.IndependenceProcessingLeanInfoTheory.Examples.InformationDecompositionLeanInfoTheory.Examples.KLTopLeanInfoTheory.Examples.StochasticChannelsLeanInfoTheory.Examples.SufficientStatisticsLeanInfoTheory.Examples.SupportSensitiveLeanInfoTheory.Examples.Units | 0 |
LeanInfoTheory.Examples.CommonCause | LeanInfoTheory.Shannon.SemanticBridge.Markov | 0 |
LeanInfoTheory.Examples.ConditionalKL | LeanInfoTheory.Shannon.SemanticBridge.ConditionalKL | 0 |
LeanInfoTheory.Examples.Convexity | LeanInfoTheory.Probability.FiniteMixtureLeanInfoTheory.Shannon.EntropyConcavityLeanInfoTheory.Shannon.LogSumLeanInfoTheory.Shannon.SemanticBridge.Convexity | 0 |
LeanInfoTheory.Examples.Fano | LeanInfoTheory.Shannon.Fano | 0 |
LeanInfoTheory.Examples.FiniteFamily | LeanInfoTheory.Shannon.EntropyBoundsLeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependence | 0 |
LeanInfoTheory.Examples.IndependenceProcessing | LeanInfoTheory.Shannon.SemanticBridge.Independence | 0 |
LeanInfoTheory.Examples.InformationDecomposition | LeanInfoTheory.Shannon.InfoMeasures | 0 |
LeanInfoTheory.Examples.KLTop | LeanInfoTheory.Shannon.SemanticBridge.KL | 0 |
LeanInfoTheory.Examples.StochasticChannels | LeanInfoTheory.Shannon.EntropyBoundsLeanInfoTheory.Shannon.SemanticBridge.DataProcessing | 0 |
LeanInfoTheory.Examples.SufficientStatistics | LeanInfoTheory.Shannon.SemanticBridge.Sufficiency.KL | 0 |
LeanInfoTheory.Examples.SupportSensitive | LeanInfoTheory.Shannon.EntropyBoundsLeanInfoTheory.Shannon.SemanticBridge.Theorems | 0 |
LeanInfoTheory.Examples.Units | LeanInfoTheory.Shannon.SemanticBridge.KLLeanInfoTheory.Shannon.Units | 0 |
LeanInfoTheory.MathlibFragments | none | 5 |
The machine-readable graph is available as
module_graph.json.