Development

Build

git clone https://github.com/serhatemrecoban/LeanInfoTheory.git
cd LeanInfoTheory
lake exe cache get
lake build LeanInfoTheory

The v0.1.0 baseline uses Lean v4.33.1 and mathlib v4.33.1.

Focused Checks

python scripts/validate_release.py
python scripts/validate_release.py focused LeanInfoTheory.Shannon.SemanticBridge

The first command is the canonical local release gate. It checks the default and maintained warning-as-error builds, the frozen public API, import boundaries, proof dependencies, generated references, website, and repository hygiene. Use the focused form while iterating on one maintained target.

Website Generation

python scripts/generate_current_public_api.py
python scripts/generate_v0_1_public_api.py --check
python scripts/generate_website_blueprint.py
python scripts/generate_website_api_index.py
python scripts/validate_release.py static

Run these after changing Lean imports, public declarations, or doc comments. They regenerate the website's module-level dependency map, source-derived declaration index, and machine-readable module/declaration JSON data. The old v0.1 generator verifies frozen bytes without writing. Current inventory does not approve import or attribute growth; those decisions belong in the reviewed current API policy. Inspect current file-linked doc-gen output directly in docbuild/.lake/build/doc/: its source-content attestation cannot be staged as frozen docs/v0.1.0/. Historical preview/release staging requires exact release source; maintenance composes a separately validated frozen route with the current site. The static gate reruns every generator in non-mutating --check mode, validates generated JSON and the tracked website, and fails if the artifacts are stale. CI uses the same gate. Release-mode staging is reserved for a clean exact- commit GitHub-source build.

Project Hygiene

• Local validation and CI share strict source, trust, API-boundary, generated-artifact, and hygiene gates.
• Core finite Shannon files keep imports light.
• Heavier KL, conditional-law, Markov, and data-processing imports live in the semantic bridge layer.
• Basic, examples, and reference anchors are non-stable and remain outside both mathematical umbrellas.

Import Guide

• Use LeanInfoTheory for the lightweight finite-PMF and information-measure API.
• Use LeanInfoTheory.Shannon for the complete supported mathematical stack.
• Use LeanInfoTheory.Shannon.Entropy for finite entropy basics.
• Use LeanInfoTheory.Shannon.InfoMeasures for marginals, conditional entropy, mutual information, and conditional mutual information.
• Use LeanInfoTheory.Shannon.FiniteFamily for dependent finite-family laws, atom entropy/MI/CMI, pair/triple bridges, and binary/ordered entropy, MI, and conditional-MI chain rules.
• Use LeanInfoTheory.Shannon.EntropyBounds when the Jensen-based upper bound or uniform equality theorem is needed.
• Use LeanInfoTheory.Probability.FiniteMixture for binary NNReal-weighted PMF mixtures and their endpoint laws.
• Use LeanInfoTheory.Shannon.LogSum for the zero-safe finite log-sum inequality and equality API.
• Use LeanInfoTheory.Shannon.EntropyConcavity for general-selector or binary entropy concavity.
• Use LeanInfoTheory.Probability.FiniteChannel for type-generic raw PMF-valued channel constructions and their elementary laws.
• Use LeanInfoTheory.Shannon.SemanticBridge for the complete opt-in expected-information, conditional-law, KL, independence, Markov, finite-family, and data-processing surface.
• Use LeanInfoTheory.Shannon.SemanticBridge.Entropy directly for self-information and the entropy-integral bridge.
• Use LeanInfoTheory.Shannon.SemanticBridge.Markov or LeanInfoTheory.Shannon.SemanticBridge.DataProcessing directly when only one heavy semantic surface is needed.
• Use LeanInfoTheory.Shannon.SemanticBridge.Convexity directly for finite-selector KL joint convexity, binary KL equality, and MI input-law concavity and channel convexity.
• Use LeanInfoTheory.Shannon.SemanticBridge.FiniteFamily directly for family Shannon inequalities.
• Use LeanInfoTheory.Shannon.SemanticBridge.ConditionalKL directly for common-base channel conditional KL, its finite weighted semantics, and joint chain rule.
• Use LeanInfoTheory.Shannon.SemanticBridge.FiniteFamilyIndependence directly for finite-atom mutual independence and the n-way entropy-equality characterization.
• The LeanInfoTheory.Examples hierarchy is maintained regression coverage, not stable 0.1.x API.
• Use LeanInfoTheory.Examples.FiniteFamily for maintained family-chain, mutual-independence, and dependent-alphabet examples.
• Use LeanInfoTheory.Examples.ConditionalKL for maintained non-public conditional-KL boundary regressions.
• Use LeanInfoTheory.Examples.Convexity for maintained non-public Section 2.7 regression consumers.

Working Notes

The living project history is tracked in docs/project-log.md. Foundation conventions live in docs/foundation-conventions.md. The signature-bearing reference is generated with pinned doc-gen4; this page and the module guide remain curated hand-written companions.

For mathlib and Lean community questions, see Lean Zulip.