Braverman's real gate approximators

Over ℝ, the conjunction of bits b₁, …, b_K is approximated by ∏_c (1 - ∑_{j ∈ S c} (1 - bⱼ)) for a family S of sets of arguments (andApprox), and the disjunction by its De Morgan dual 1 - ∏_c (1 - ∑_{j ∈ S c} bⱼ) (orApprox). At bits, a factor is 1 minus the number of zeros in its set, so the approximator is exact unless some argument is 0 and no set contains exactly one zero (AndMiss, andApprox_bitVal). Negation is exactly 1 - b. Each approximator multiplies degrees by the number of sets (gateApprox_mem_lowDegree) and its values stay bounded on bounded arguments (abs_andApprox_le, abs_orApprox_le, abs_gateApprox_le).

Following Braverman, Lemma 8, take s sets at each of the rates 2⁻¹, …, 2⁻ℓ. When the arguments have z ≥ 1 zeros and 2 ^ r ≤ z < 2 ^ (r + 1), a random set of rate p = 2 ^ -(r + 1) contains exactly one zero with probability z p (1 - p) ^ (z - 1) ≥ 1 / (2e) > 9 / 50. So the s sets of that rate all miss with probability at most (41 / 50) ^ s, and averaging over the sets against any weights ν on the inputs fixes sets whose misses have weight at most (41 / 50) ^ s times the total (exists_sum_gateMiss_le). Braverman pads the fan-in to k = 2 ^ ℓ and also needs the rate 1 / (2k) when all k arguments are 0; here the fan-in is assumed to be less than 2 ^ ℓ, which avoids that case. We choose the sets greedily, one at a time, each by an average over a single random set; the constant 41 / 50 is Braverman's 0.82.

The sup-norm bounds are our own; they replace Braverman, Proposition 9 in the circuit-level approximation (Braverman.exists_lowDegree_approx).

Main definitions

• Cslib.Circuits.Boolean.Braverman.andApprox, Cslib.Circuits.Boolean.Braverman.orApprox, Cslib.Circuits.Boolean.Braverman.gateApprox: the real approximators for a family of sets.
• Cslib.Circuits.Boolean.Braverman.AndMiss, Cslib.Circuits.Boolean.Braverman.GateMiss: the bits at which an approximator may err.

Main results

• Cslib.Circuits.Boolean.Braverman.gateApprox_bitVal: exactness away from misses.
• Cslib.Circuits.Boolean.Braverman.gateApprox_mem_lowDegree: the degree bound.
• Cslib.Circuits.Boolean.Braverman.abs_gateApprox_le: the sup-norm bound.
• Cslib.Circuits.Boolean.Braverman.exists_sum_gateMiss_le: Braverman's choice of sets.

References

• M. Braverman, Polylogarithmic independence fools AC⁰ circuits

noncomputable def Cslib.Circuits.Boolean.Braverman.andApprox {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) (v : Fin K → ℝ) : ℝ

Braverman's AND approximator for a family S of sets of arguments: the product over the sets of 1 - ∑_{j ∈ S c} (1 - v j) Braverman, Lemma 8.

noncomputable def Cslib.Circuits.Boolean.Braverman.orApprox {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) (v : Fin K → ℝ) : ℝ

The OR approximator, the De Morgan dual of andApprox (orApprox_eq).

theorem Cslib.Circuits.Boolean.Braverman.orApprox_eq {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) (v : Fin K → ℝ) : orApprox S v = 1 - andApprox S fun (j : Fin K) => 1 - v j

The OR approximator is the De Morgan dual of the AND approximator.

def Cslib.Circuits.Boolean.Braverman.AndMiss {κ : Type u_1} {K : ℕ} (S : κ → Fin K → Bool) (b : Fin K → Bool) : Prop

The AND approximator for S misses at the bits b when some bit is false but no set of S contains exactly one false bit.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Braverman.instDecidableAndMiss {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) (b : Fin K → Bool) : Decidable (AndMiss S b)

theorem Cslib.Circuits.Boolean.Braverman.andApprox_bitVal {κ : Type u_1} [Fintype κ] {K : ℕ} {S : κ → Fin K → Bool} {b : Fin K → Bool} (h : ¬AndMiss S b) : (andApprox S fun (j : Fin K) => BitString.bitVal ℝ (b j)) = BitString.bitVal ℝ (decide (∀ (j : Fin K), b j = true))

Exactness of the AND approximator at bits where it does not miss.

theorem Cslib.Circuits.Boolean.Braverman.orApprox_bitVal {κ : Type u_1} [Fintype κ] {K : ℕ} {S : κ → Fin K → Bool} {b : Fin K → Bool} (h : ¬AndMiss S fun (j : Fin K) => !b j) : (orApprox S fun (j : Fin K) => BitString.bitVal ℝ (b j)) = BitString.bitVal ℝ (decide (∃ (j : Fin K), b j = true))

Exactness of the OR approximator at bits whose negations the AND approximator does not miss.

theorem Cslib.Circuits.Boolean.Braverman.andApprox_mem_lowDegree {κ : Type u_1} [Fintype κ] {K : ℕ} {ι : Type u_2} {D : ℕ} (S : κ → Fin K → Bool) {v : Fin K → (ι → Bool) → ℝ} (hv : ∀ (j : Fin K), v j ∈ BitString.lowDegree ℝ ι D) : (fun (x : ι → Bool) => andApprox S fun (j : Fin K) => v j x) ∈ BitString.lowDegree ℝ ι (Fintype.card κ * D)

The AND approximator multiplies degrees by the number of sets.

theorem Cslib.Circuits.Boolean.Braverman.orApprox_mem_lowDegree {κ : Type u_1} [Fintype κ] {K : ℕ} {ι : Type u_2} {D : ℕ} (S : κ → Fin K → Bool) {v : Fin K → (ι → Bool) → ℝ} (hv : ∀ (j : Fin K), v j ∈ BitString.lowDegree ℝ ι D) : (fun (x : ι → Bool) => orApprox S fun (j : Fin K) => v j x) ∈ BitString.lowDegree ℝ ι (Fintype.card κ * D)

The OR approximator multiplies degrees by the number of sets.

theorem Cslib.Circuits.Boolean.Braverman.abs_andApprox_le {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) {v : Fin K → ℝ} {B : ℝ} (hB : 0 ≤ B) (hv : ∀ (j : Fin K), |v j| ≤ B) : |andApprox S v| ≤ (1 + ↑K * (1 + B)) ^ Fintype.card κ

Sup-norm bound for the AND approximator.

theorem Cslib.Circuits.Boolean.Braverman.abs_orApprox_le {κ : Type u_1} [Fintype κ] {K : ℕ} (S : κ → Fin K → Bool) {v : Fin K → ℝ} {B : ℝ} (hB : 0 ≤ B) (hv : ∀ (j : Fin K), |v j| ≤ B) : |orApprox S v| ≤ 1 + (1 + ↑K * B) ^ Fintype.card κ

Sup-norm bound for the OR approximator.

noncomputable def Cslib.Circuits.Boolean.Braverman.gateApprox {κ : Type u_1} [Fintype κ] (op : Unbounded.Op) : (κ → Fin op.arity → Bool) → (Fin op.arity → ℝ) → ℝ

The approximator of a gate of the unbounded fan-in basis for a family S of sets of its arguments: 1 - v for negation, andApprox and orApprox for conjunction and disjunction.

def Cslib.Circuits.Boolean.Braverman.GateMiss {κ : Type u_1} (op : Unbounded.Op) : (κ → Fin op.arity → Bool) → (Fin op.arity → Bool) → Prop

The bits at which the approximator of a gate may err: never for negation, and AndMiss for conjunction and, at the negated bits, for disjunction.

@[instance_reducible]

instance Cslib.Circuits.Boolean.Braverman.instDecidableGateMiss {κ : Type u_1} [Fintype κ] (op : Unbounded.Op) (S : κ → Fin op.arity → Bool) (b : Fin op.arity → Bool) : Decidable (GateMiss op S b)

theorem Cslib.Circuits.Boolean.Braverman.gateApprox_bitVal {κ : Type u_1} [Fintype κ] {op : Unbounded.Op} {S : κ → Fin op.arity → Bool} {b : Fin op.arity → Bool} (h : ¬GateMiss op S b) : (gateApprox op S fun (j : Fin op.arity) => BitString.bitVal ℝ (b j)) = BitString.bitVal ℝ (Unbounded.interpretation op b)

Exactness of the gate approximators at bits where they do not miss.

theorem Cslib.Circuits.Boolean.Braverman.gateApprox_mem_lowDegree {κ : Type u_1} [Fintype κ] {ι : Type u_2} {D : ℕ} (hκ : 1 ≤ Fintype.card κ) (op : Unbounded.Op) (S : κ → Fin op.arity → Bool) {v : Fin op.arity → (ι → Bool) → ℝ} (hv : ∀ (j : Fin op.arity), v j ∈ BitString.lowDegree ℝ ι D) : (fun (x : ι → Bool) => gateApprox op S fun (j : Fin op.arity) => v j x) ∈ BitString.lowDegree ℝ ι (Fintype.card κ * D)

Degrees of the gate approximators: a gate with a nonempty family of sets multiplies degrees by the number of sets.

theorem Cslib.Circuits.Boolean.Braverman.abs_gateApprox_le {κ : Type u_1} [Fintype κ] {ℓ E : ℕ} (hκ : 1 ≤ Fintype.card κ) (op : Unbounded.Op) (hop : op.arity < 2 ^ ℓ) (S : κ → Fin op.arity → Bool) {v : Fin op.arity → ℝ} (hv : ∀ (j : Fin op.arity), |v j| ≤ 2 ^ E) : |gateApprox op S v| ≤ 2 ^ (Fintype.card κ * (E + ℓ + 1))

Sup-norm bound for the gate approximators (our bound, replacing Braverman, Proposition 9): with a nonempty family of t sets, a gate of fan-in less than 2 ^ ℓ on arguments of absolute value at most 2 ^ E has absolute value at most 2 ^ (t (E + ℓ + 1)).

Choosing the sets

theorem Cslib.Circuits.Boolean.Braverman.exists_sum_andMiss_le {K ℓ s : ℕ} {X : Type u_1} [Fintype X] (hK : K < 2 ^ ℓ) (ν : X → ℝ) (hν : ∀ (x : X), 0 ≤ ν x) (u : X → Fin K → Bool) : ∃ (S : Fin (ℓ * s) → Fin K → Bool), ∑ x : X with AndMiss S (u x), ν x ≤ (41 / 50) ^ s * ∑ x : X, ν x

Braverman's choice of sets for an AND gate Braverman, Lemma 8: for every nonnegative weights ν on a finite set of points, at which the K < 2 ^ ℓ arguments of the gate take the values u x, there are s sets at each of the rates 2⁻¹, …, 2⁻ℓ whose misses have weight at most (41 / 50) ^ s times the total.

theorem Cslib.Circuits.Boolean.Braverman.exists_sum_gateMiss_le {ℓ s : ℕ} {X : Type u_1} [Fintype X] (ν : X → ℝ) (hν : ∀ (x : X), 0 ≤ ν x) (op : Unbounded.Op) (hop : op.arity < 2 ^ ℓ) (u : X → Fin op.arity → Bool) : ∃ (S : Fin (ℓ * s) → Fin op.arity → Bool), ∑ x : X with GateMiss op S (u x), ν x ≤ (41 / 50) ^ s * ∑ x : X, ν x

Braverman's choice of sets for a gate Braverman, Lemma 8: for every nonnegative weights ν on a finite set of points, at which the arguments of a gate of fan-in less than 2 ^ ℓ take the values u x, there are s sets at each of the rates 2⁻¹, …, 2⁻ℓ whose misses have weight at most (41 / 50) ^ s times the total.