Braverman's approximation of circuits with an AC⁰ witness

For every distribution ν on the inputs, a circuit C of the unbounded fan-in basis, of depth d and fan-in less than 2 ^ ℓ, agrees with a real function f of degree at most (ℓ s) ^ d except where a witness circuit W outputs 1, and W outputs 1 with ν-probability at most (41 / 50) ^ s · size C (exists_lowDegree_approx) Braverman, Lemma 8. The function f is bounded by 2 ^ (2 (ℓ + 1) ((ℓ s) ^ d - 1)) everywhere, which plays the role of Braverman, Proposition 9, and W has depth at most d + 6 and an explicit size.

As in Smolensky's approximation (Smolensky.exists_lowDegree_approx), the circuit is evaluated on pairs of a true function and its approximant. An operation applied to pairs computes the true function of its arguments and applies the approximator of exists_sum_gateMiss_le, with sets chosen for ν and for these true arguments, to their approximants. The approximants are exact at every input where no gate of depth at most d misses on its true arguments. Whether a gate misses is decided from the values of the wires it reads by a formula of depth 5 (no set contains exactly one zero, and some argument is zero), so the witness is the disjunction of these formulas, fed by the wires of C.

The sup-norm bound, the witness's size size C · ((ℓ s + 1) (r + 1) ^ 2 + 3) + 1 for fan-in at most r, and its depth d + 6, where depth counts negations as in Circuit.depth, are our own; Braverman states size O(m² r) and depth < d + 3 for his witness, in a model where negations are free. Only the gates of depth at most d are checked, so that gates that do not feed the output cannot make the witness deeper.

Main results

• Cslib.Circuits.Boolean.Braverman.exists_lowDegree_approx: Braverman's approximation with a witness circuit.

References

• M. Braverman, Polylogarithmic independence fools AC⁰ circuits

Approximants on pairs

The witness formula

The witness circuit

theorem Cslib.Circuits.Boolean.Braverman.exists_lowDegree_approx {n : ℕ} (ν : PMF (BitString n)) {ℓ s r : ℕ} (hℓs : 2 ≤ ℓ * s) (hr : r < 2 ^ ℓ) (C : Circuit Unbounded.signature n 1) (hC : C.FanInAtMost r) : ∃ f ∈ BitString.lowDegree ℝ (Fin n) ((ℓ * s) ^ C.depth), (∀ (x : Fin n → Bool), |f x| ≤ 2 ^ (2 * (ℓ + 1) * ((ℓ * s) ^ C.depth - 1))) ∧ ∃ (W : Circuit Unbounded.signature n 1), W.size ≤ C.size * ((ℓ * s + 1) * (r + 1) ^ 2 + 3) + 1 ∧ W.depth ≤ C.depth + 6 ∧ ∑ x : Fin n → Bool with W.eval Unbounded.interpretation x 0 = true, (ν x).toReal ≤ (41 / 50) ^ s * ↑C.size ∧ ∀ (x : Fin n → Bool), W.eval Unbounded.interpretation x 0 = false → f x = BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)

Braverman's approximation Braverman, Lemma 8. Let ν be a distribution on the inputs and C a circuit of the unbounded fan-in basis of fan-in at most r < 2 ^ ℓ, and let 2 ≤ ℓ s. Some real function f of degree at most (ℓ s) ^ depth C, bounded by 2 ^ (2 (ℓ + 1) ((ℓ s) ^ depth C - 1)), agrees with C wherever a witness circuit W outputs false, and W outputs true with ν-probability at most (41 / 50) ^ s · size C. The witness has depth at most depth C + 6 and size at most size C · ((ℓ s + 1) (r + 1) ^ 2 + 3) + 1.

The sup-norm bound replaces Braverman, Proposition 9, and the size and depth of the witness are our own count, in the model of Circuit.depth, where negations count.