The Linial–Mansour–Nisan theorem

A function computed by a small circuit of constant depth with unbounded fan-in has almost all of its Fourier weight on small sets of coordinates [LMN93], O'Donnell, Section 4.5: for a circuit of depth d with g gates, s ≥ 2 and n ≥ 1, the weight on the sets of at least k coordinates is at most 2 g / 2 ^ s once max 8 (2 s) n ≤ k ⌊n / (16 s + 1) ^ d⌋ (Unbounded.sum_fourierCoeff_sq_le_of_computes). For fixed d it is g 2 ^ (-Ω(k ^ (1 / (d + 1)))): the exponent is weaker than the k ^ (1 / d) of Linial, Mansour and Nisan, since depth counts every gate on a path, negations included, and each stage leaves a 1 / (16 s + 1) fraction of the free bits (as in Unbounded.two_pow_le_size_of_computes_parity).

The proof draws a random set J of ℓ = ⌊n / (16 s + 1) ^ d⌋ coordinates and fixes the others to a random word z, a random restriction (partial assignment) (PartialAssignment.sum_card_filter_outside). A set U of at least k coordinates meets J in at least s of them for at least half of the J (Finset.two_mul_card_filter_card_inter_lt_le), so the weight on such U is at most twice the expected weight of the restriction on sets of at least s coordinates (BitString.expect_sum_fourierCoeff_piecewise_sq). That is zero when the restriction has a decision tree of depth below s (DecisionTree.fourierCoeff_eq_zero_of_depth_lt) and at most one otherwise (Parseval), and the restriction is deep with probability at most g / 2 ^ s (Unbounded.two_pow_mul_card_filter_exists_not_shallow_le).

Main results

• Cslib.Circuits.Boolean.Unbounded.sum_fourierCoeff_sq_le_of_computes: the Linial–Mansour–Nisan theorem.
• Cslib.Circuits.Boolean.Unbounded.sum_fourierCoeff_sq_le_of_computes_of_depth_le: the bound above the explicit degree 2 max 8 (2 s) (16 s + 1) ^ d - 1, for every number of inputs.

References

• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability
• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.Circuits.Boolean.Unbounded.sum_fourierCoeff_sq_le_of_computes {n : ℕ} {f : BooleanFunction n} {C : Circuit signature n 1} (hC : C.Computes interpretation (single f)) {s : ℕ} (hs : 2 ≤ s) (hn0 : 0 < n) {k : ℕ} (hk : max 8 (2 * s) * n ≤ k * (n / (16 * s + 1) ^ C.depth)) : ∑ U : Finset (Fin n) with k ≤ U.card, BitString.fourierCoeff (fun (x : Fin n → Bool) => BitString.signVal (f x)) U ^ 2 ≤ 2 * ↑C.size / 2 ^ s

The Linial–Mansour–Nisan theorem. Let f be computed by a circuit of negations and unbounded fan-in conjunctions and disjunctions of depth d with g gates, let s ≥ 2 and n ≥ 1, and let ℓ = ⌊n / (16 s + 1) ^ d⌋. Then the Fourier weight of f, read as ±1, on the sets of at least k coordinates is at most 2 g / 2 ^ s, whenever max 8 (2 s) n ≤ k ℓ.

theorem Cslib.Circuits.Boolean.Unbounded.sum_fourierCoeff_sq_le_of_computes_of_depth_le {n : ℕ} {f : BooleanFunction n} {C : Circuit signature n 1} (hC : C.Computes interpretation (single f)) {s d t : ℕ} (hs : 2 ≤ s) (hd : C.depth ≤ d) (ht : 2 * max 8 (2 * s) * (16 * s + 1) ^ d ≤ t + 1) : ∑ U : Finset (Fin n) with t < U.card, BitString.fourierCoeff (fun (x : Fin n → Bool) => BitString.signVal (f x)) U ^ 2 ≤ 2 * ↑C.size / 2 ^ s

The Linial–Mansour–Nisan theorem above an explicit degree. Let f be computed by a circuit of negations and unbounded fan-in conjunctions and disjunctions of depth at most d, and let s ≥ 2. Then the Fourier weight of f, read as signs, on the sets of more than t coordinates is at most 2 g / 2 ^ s, where g is the number of gates, whenever 2 max 8 (2 s) (16 s + 1) ^ d ≤ t + 1.