Start with a released library, not a blank file. LeanInfoTheory gives your Lean project a substantial, reusable foundation for finite discrete information theory.

Install the stable release

These guides target LeanInfoTheory v0.1.0, with Lean and mathlib v4.33.1. You need Lean's Elan/Lake toolchain and Git. For a new project, create a Lean library project with Lake or your editor; for an existing project, check dependency compatibility first.

Set your project's lean-toolchain to:

leanprover/lean4:v4.33.1

Add this dependency to lakefile.toml:

[[require]]
name = "LeanInfoTheory"
git = "https://github.com/serhatemrecoban/LeanInfoTheory"
rev = "v0.1.0"

From your project directory, resolve dependencies, retrieve the mathlib cache, and build:

lake update
lake exe cache get
lake build

The release fixes its toolchain. Do not mix incompatible Lean or mathlib versions, and do not replace the version tag with master for a reproducible research project.

Prove your first result

A deterministic law has zero entropy. This is a complete Lean example:

import LeanInfoTheory

open LeanInfoTheory.Shannon

example : entropy (PMF.pure false) = 0 := by
  exact entropy_pure false

Put the example in a Lean file in your project and check it with your editor or lake env lean YourFile.lean. The library supplies the theorem; your proof applies it to the law concentrated at false.

Choose an import

import LeanInfoTheory gives you the lightweight PMF and elementary information-measure layer. import LeanInfoTheory.Shannon loads the complete supported mathematical stack. For a smaller dependency closure, use the focused module guide.

Where next?