Analysis of Boolean Functions in Lean

 Analysis of Boolean Functions in Lean🔗

Compiled2026-08-30T19:38:18ZProject164f830fix: use memoir-compatible math font commandLeanleanprover/lean4:v4.32.0VersoBlueprintv4.32.0@51ebcae4b313Mathlibv4.32.0@81a5d257c8e4

This Blueprint follows the May 2021 edition of Ryan O'Donnell's Analysis of Boolean Functions and uses its ordering and notation.

The graph below records the mathematical dependencies among the definitions and results.

Contents

  1. 1. Boolean functions and the Fourier expansion
  2. 2. Influence and noise sensitivity
  3. 3. Spectral structure and learning
  4. 4. DNF formulas and small-depth circuits
  5. 5. Majority and threshold functions
  6. 6. Pseudorandomness and F₂-polynomials
  7. 7. Property testing, PCPPs, and CSPs
  8. 8. Generalized domains
  9. 9. Basics of hypercontractivity
  10. Dependency Graph