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

  1. Install Lean 4 and dependencies as explained here.

  2. 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):

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.