Analysis of Boolean functions in Lean
This is a project formalizing some basic definitions and results in the analysis of Boolean functions using Lean 4, largely following the book Analysis of Boolean functions by Ryan O'Donnell.
Main results formalized so far:
- Plancherel's theorem for the Walsh-Fourier transform
- L² Poincaré inequality
- Blum-Luby-Rubinfeld linearity testing
- a version of Arrow's theorem
Installation
-
Install Lean 4 and dependencies as explained here.
-
Clone this repository using
git clone https://github.com/roos-j/lean-booleanfun.git
and open it in VS Code (more instructions here).
Future goals
- hypercontractivity, Bonami lemma
- KKL theorem
- Bobkov's two-point inequality
- Talagrand's isoperimetric theorem
- FKN theorem
Note: the central limit theorem will be needed eventually; currently not in Mathlib
Todo
- add doc-gen4
- streamline proofs
Previous formalizations of Arrow's theorem
Arrow's theorem has been formalized before (and in more general formulations):
- in Mizar by Freek Wiedijk
- in Isabelle/HOL by Tobias Nipkow
- in Lean by Andrew Souther, Benjamin Davidson
These formalizations use direct combinatorial arguments of John Geanakoplos.
The formalization in this project uses Gil Kalai's Fourier-analytic approach as in Sec. 2.5 of Ryan O'Donnell's book.