Section 6.4, “AC0 has little high-frequency mass”Linial–Mansour–Nisan and Tal: AC0 functions have little Fourier mass above low degree
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
has little high-frequency mass. A seminal theorem of Linial–Mansour–Nisan shows that functions have almost all Fourier mass on low degrees: for computed by an circuit of size , the tail above degree decays rapidly with (see (Linial et al., 1993), and sharper bounds in (Tal, 2015)). For fixed depth and polynomial size, correlation with full parity under the uniform distribution is negligible in . Applying this statement to other subsets requires specifying their size relative to circuit depth and size, and it does not automatically apply under a nonuniform training distribution.
Generated from paper_jmlr.tex, lines 969–972.
2 Explain this
A classical theorem (Linial, Mansour and Nisan; sharpened by Tal): functions computed by constant-depth, polynomial-size circuits have almost all of their Fourier mass at low degree. Consequently their correlation with full parity is negligible.
Caveats in the paper. Applying this to parities of other subsets requires relating the subset size to the circuit depth and size, and the uniform-distribution statement does not automatically transfer to a nonuniform training distribution.
3 How this is formalised
Cited, not proved. In Lean the corresponding hypothesis is the named Fourier.TailPremise, used only in
a conditional application. Matching it to a precise published statement is an open item
(Section 10, paragraph 3 (open item)). The main single-channel bound does not use it.
| Paper anchor | par-ac0-has-little-high-frequency-mass-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 6.4, “AC0 has little high-frequency mass” |
| Claim | Linial–Mansour–Nisan and Tal: AC0 functions have little Fourier mass above low degree |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 969–972; SHA-256 of the normalised block source cc00adcaa05b249d… |
| Depends on | Section 10, paragraph 3 (open item) |
| Explanations | explain/c-lmn, formal/c-lmn |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is a published classical result. It is cited, not proved in this Lean development.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).