Analysis of Boolean functions #
Aggregation module for the Fourier analysis of Boolean functions, following Ryan
O'Donnell's Analysis of Boolean Functions. This subtheory grows inside the
larger complexity-theory corpus, where the Fourier-analytic toolkit underpins
circuit lower bounds (small-depth circuits, AC⁰), learning, property testing,
and the natural-proofs barrier.
Currently formalized: Boolean functions and the Fourier expansion, with the
parity functions as an orthonormal basis, Fourier coefficients and weights,
Parseval/Plancherel, and the mean/variance/covariance and convolution API;
Chapter 2 foundations include noise stability, the noise operator, derivatives,
and coordinate and total influence. All definitions and theorems live under the
Complexity.BooleanAnalysis namespace.