Analysis of Boolean Functions in Lean

 Analysis of Boolean Functions in Lean🔗

Compiled2026-07-12T20:16:22ZProject34334a1ci: fetch Mathlib cache for Blueprint subproject and deploy to GitHub PagesLeanleanprover/lean4:v4.30.0VersoBlueprintv4.30.0@f8e18142eb1bMathlibv4.30.0@c5ea00351c28

FABL formalizes the May 2021 edition of Ryan O'Donnell's Analysis of Boolean Functions in Lean 4 and Mathlib. The present volume covers Chapters 1--3.

Each entry gives the book-facing statement and its associated Lean declarations. The graph below records the mathematical dependencies between results.

Contents

  1. 1. Boolean functions and the Fourier expansion
  2. 2. Influence and noise sensitivity
  3. 3. Spectral structure and learning
  4. Dependency Graph