Polylogarithmic independence fools AC⁰

A k-wise independent distribution on the inputs fools every circuit of the unbounded fan-in basis of constant depth, once k is polylogarithmic in the size of the circuit and in the inverse of the error Braverman, Main Theorem.

The proof follows Braverman. Approximate the circuit C (exists_lowDegree_approx), for the average of the k-wise independent distribution X and the uniform distribution, by a real function f of degree at most (ℓ s) ^ d that agrees with C wherever a witness circuit W is false; W is then true with probability at most 2 (41 / 50) ^ s · size C under both X and the uniform distribution. The witness is again a circuit of constant depth, so its 0/1 reading has a low-degree L² approximation whenever its Fourier weight above some level t is small (exists_mem_lowDegree_expect_sq_bitVal_sub_eq). Braverman's mollification, squaring trick and one-sided chain (IsKWiseIndependent.fools_bitVal_of_witness) then show that X fools C once 2 ((ℓ s) ^ d + t) ≤ k. Braverman obtains the other direction by applying his Lemma 12 to 1 - C with a fresh approximation; reusing f and the witness through 1 - f is our variant (it avoids a NOT layer).

The result is first stated with the Fourier tail of the witness circuits as a hypothesis (fools_of_isKWiseIndependent_of_tail), in the parametric form of Tal, Theorem 20. The Linial–Mansour–Nisan theorem of this library (Unbounded.sum_fourierCoeff_sq_le_of_computes_of_depth_le) discharges the hypothesis: if C has depth at most d, at most 2 ^ q gates and fan-in less than 2 ^ q, then every independence d q-wise independent distribution 2 ^ (-q)-fools C (fools_of_independence_le), and independence d q ≤ (64 q) ^ ((2 d + 3) (d + 7) + 1) (independence_le, fools_of_isKWiseIndependent). Taking q ≥ log₂ (fan-in + 1) and q at least log₂ of the size and of the inverse of the error, k = (log (m / ε)) ^ O(d²) independence suffices for circuits of size m with fan-in at most m, which is the form of Braverman's theorem.

The constants are our own and are weaker than Braverman's, since the Linial–Mansour–Nisan theorem of this library has exponent 1 / (d + 1) and depth counts negations (Circuit.depth).

Main definitions

• Cslib.Circuits.Boolean.Braverman.level, Cslib.Circuits.Boolean.Braverman.independence: the level of the Fourier tail and the independence used by fools_of_independence_le.

Main results

• Cslib.Circuits.Boolean.Braverman.fools_of_isKWiseIndependent_of_tail: Braverman's theorem with the Fourier tail of the witness circuits as a hypothesis.
• Cslib.Circuits.Boolean.Braverman.fools_of_independence_le: polylogarithmic independence fools AC⁰, with the sharp independence independence d q.
• Cslib.Circuits.Boolean.Braverman.fools_of_isKWiseIndependent: polylogarithmic independence fools AC⁰, with the closed-form independence (64 q) ^ ((2 d + 3) (d + 7) + 1).

References

• M. Braverman, Polylogarithmic independence fools AC⁰ circuits
• A. Tal, Tight bounds on the Fourier spectrum of AC⁰
• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability

The average with the uniform distribution

Braverman's theorem with a Fourier tail hypothesis

theorem Cslib.Circuits.Boolean.Braverman.fools_of_isKWiseIndependent_of_tail {n : ℕ} {X : PMF (BitString n)} {ℓ s r d t k : ℕ} {τ : ℝ} (hℓs : 2 ≤ ℓ * s) (hr : r < 2 ^ ℓ) (C : Circuit Unbounded.signature n 1) (hC : C.FanInAtMost r) (hd : C.depth ≤ d) (htail : ∀ (W : Circuit Unbounded.signature n 1), W.size ≤ C.size * ((ℓ * s + 1) * (r + 1) ^ 2 + 3) + 1 → W.depth ≤ d + 6 → ∑ U : Finset (Fin n) with t < U.card, BitString.fourierCoeff (fun (x : Fin n → Bool) => BitString.signVal (W.eval Unbounded.interpretation x 0)) U ^ 2 ≤ τ) (hk : 2 * ((ℓ * s) ^ d + t) ≤ k) (hX : BitString.IsKWiseIndependent k X) : BitString.Fools X (8 * (41 / 50) ^ s * ↑C.size + (2 ^ (2 * (ℓ + 1) * ((ℓ * s) ^ d - 1)) + 1) ^ 2 * τ / 2) fun (x : Fin n → Bool) => BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)

Braverman's theorem with a Fourier tail hypothesis Braverman, Main Theorem, in the parametric form of Tal, Theorem 20. Let C be a circuit of the unbounded fan-in basis of depth at most d and fan-in at most r < 2 ^ ℓ, let 2 ≤ ℓ s, and suppose every circuit of depth at most d + 6 and size at most size C · ((ℓ s + 1) (r + 1) ^ 2 + 3) + 1 has Fourier weight, read as signs, at most τ above level t. Then every k-wise independent distribution with 2 ((ℓ s) ^ d + t) ≤ k fools C with error 8 (41 / 50) ^ s · size C + (2 ^ (2 (ℓ + 1) ((ℓ s) ^ d - 1)) + 1) ^ 2 τ / 2.

The size and depth of the witness circuits and the constants are our own count.

Polylogarithmic independence

def Cslib.Circuits.Boolean.Braverman.level (d q : ℕ) : ℕ

The level σ = 4 (q + 1) A ^ d + A + 4 q + 5, with A = q (8 q + 16), at which the Linial–Mansour–Nisan theorem is applied in fools_of_independence_le.

def Cslib.Circuits.Boolean.Braverman.independence (d q : ℕ) : ℕ

The independence 2 (A ^ d + 4 σ (16 σ + 1) ^ (d + 6)), with A = q (8 q + 16) and σ = level d q, that suffices in fools_of_independence_le.

theorem Cslib.Circuits.Boolean.Braverman.independence_le {q : ℕ} (hq : 1 ≤ q) (d : ℕ) : independence d q ≤ (64 * q) ^ ((2 * d + 3) * (d + 7) + 1)

The independence of fools_of_independence_le is at most (64 q) ^ ((2 d + 3) (d + 7) + 1), polynomial in q with exponent quadratic in d.

theorem Cslib.Circuits.Boolean.Braverman.fools_of_independence_le {n : ℕ} {X : PMF (BitString n)} {d q k : ℕ} (hq : 1 ≤ q) (C : Circuit Unbounded.signature n 1) (hfan : C.FanInAtMost (2 ^ q - 1)) (hsize : C.size ≤ 2 ^ q) (hd : C.depth ≤ d) (hk : independence d q ≤ k) (hX : BitString.IsKWiseIndependent k X) : BitString.Fools X (1 / 2 ^ q) fun (x : Fin n → Bool) => BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)

Polylogarithmic independence fools AC⁰, with the sharp independence Braverman, Main Theorem. Let C be a circuit of the unbounded fan-in basis of depth at most d, with at most 2 ^ q gates, each of fan-in less than 2 ^ q, where q ≥ 1. Then every k-wise independent distribution on the inputs with independence d q ≤ k fools C with error 2 ^ (-q). The independence is at most (64 q) ^ ((2 d + 3) (d + 7) + 1) (independence_le, fools_of_isKWiseIndependent).

theorem Cslib.Circuits.Boolean.Braverman.fools_of_isKWiseIndependent {n : ℕ} {X : PMF (BitString n)} {d q k : ℕ} (hq : 1 ≤ q) (C : Circuit Unbounded.signature n 1) (hfan : C.FanInAtMost (2 ^ q - 1)) (hsize : C.size ≤ 2 ^ q) (hd : C.depth ≤ d) (hk : (64 * q) ^ ((2 * d + 3) * (d + 7) + 1) ≤ k) (hX : BitString.IsKWiseIndependent k X) : BitString.Fools X (1 / 2 ^ q) fun (x : Fin n → Bool) => BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)

Polylogarithmic independence fools AC⁰ Braverman, Main Theorem. Let C be a circuit of the unbounded fan-in basis of depth at most d, with at most 2 ^ q gates, each of fan-in less than 2 ^ q, where q ≥ 1. Then every k-wise independent distribution on the inputs with k ≥ (64 q) ^ ((2 d + 3) (d + 7) + 1) fools C with error 2 ^ (-q).

Taking q ≥ log₂ (fan-in + 1) and q at least log₂ of the size and of the inverse of the error, this is the form k = (log (m / ε)) ^ O(d²) of Braverman's theorem; the explicit exponent and constants are our own, and depth counts negations (Circuit.depth).