Documentation

Complexity.Computability.Circuit.Boolean.Braverman.Resilience

Resilient functions under bounded independence #

Chattopadhyay and Zuckerman observe that Braverman's theorem transfers resilience from the uniform distribution to every distribution of polylogarithmic independence, for functions computed by monotone AC⁰ circuits Chattopadhyay–Zuckerman, Theorem 4.1. The bias carries over directly. For the influence of a coalition Q, monotonicity shows that f is undetermined at x by the bits outside Q exactly when f is true with all of Q set to true and false with all of Q set to false (Cslib.BitString.isUndetermined_iff_of_monotone). This event is computed by a constant-depth circuit E_Q (undeterminedCircuit), and Braverman's theorem applied to E_Q bounds its probability.

The circuit E_Q is our construction in the unbounded fan-in basis: it runs two copies of the circuit C on the inputs with the bits of Q fixed (fixCircuit, a restriction circuit Cslib.Circuits.Boolean.Unbounded.restrictCircuit) and combines them by a circuit of two gates computing x₀ ∧ ¬x₁. If C has m gates, depth d and fan-in r, then E_Q has exactly 2 m + 6 gates, depth at most d + 3 and fan-in at most max r 2. Chattopadhyay and Zuckerman compute ¬(C₀ = C₁) instead, with size 4 m + 3 and depth d + 2, reduced to d + 1 Chattopadhyay–Zuckerman, proof of Theorem 4.1; our count of depth includes negations and the constant gates (Circuit.depth), and C₁ ∧ ¬C₀ suffices since C₀ ≤ C₁ for monotone C.

The required independence is that of the library's Braverman theorem (Cslib.Circuits.Boolean.Braverman.fools_of_independence_le) at depth d + 3: with error 2 ^ (-p) it is at most (64 p) ^ ((2 d + 9) (d + 10) + 1). The theorem needs 2 m + 6 ≤ 2 ^ p for a circuit of m gates and, since the fan-in of this model is not bounded by the size, fan-in r < 2 ^ p; taking p ≥ max (log₂ (2 m + 6)) (max (log₂ (r + 1)) (log₂ (1 / ε))) gives t = (log (max m (r + 1) / ε)) ^ O(d²). Chattopadhyay and Zuckerman obtain (log (m / ε)) ^ (3 d + 6) from Tal's form of Braverman's theorem; that exponent is not claimed here. Monotonicity is assumed of the computed function, which is weaker than their assumption of a monotone circuit. The statements for almost t-wise independent distributions in their Theorem 4.1, which need a further approximation theorem, are not formalized.

Main definitions #

Main results #

References #

The circuit E_Q #

source
def Cslib.Circuits.Boolean.Braverman.fixCircuit {n : ℕ} (Q : Finset (Fin n)) (b : Bool) :
Circuit Unbounded.signature n n

The circuit that outputs its inputs with the bits of Q replaced by the constant b: the restriction circuit of the partial assignment fixing Q to b.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Braverman.eval_fixCircuit {n : ℕ} (Q : Finset (Fin n)) (b : Bool) (x : BitString n) :
    (fixCircuit Q b).eval Unbounded.interpretation x = Q.piecewise (fun (x : Fin n) => b) x

    fixCircuit Q b sets the bits of Q to b.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.Braverman.size_fixCircuit {n : ℕ} (Q : Finset (Fin n)) (b : Bool) :
    (fixCircuit Q b).size = 2

    fixCircuit Q b has two gates, one for each constant.

    source
    theorem Cslib.Circuits.Boolean.Braverman.depth_fixCircuit_le {n : ℕ} (Q : Finset (Fin n)) (b : Bool) :
    (fixCircuit Q b).depth ≤ 1

    fixCircuit Q b has depth at most one.

    source
    theorem Cslib.Circuits.Boolean.Braverman.fanInAtMost_fixCircuit {n : ℕ} (Q : Finset (Fin n)) (b : Bool) :
    (fixCircuit Q b).FanInAtMost 2

    fixCircuit Q b has fan-in at most two.

    source
    def Cslib.Circuits.Boolean.Braverman.undeterminedCircuit {n : ℕ} (C : Circuit Unbounded.signature n 1) (Q : Finset (Fin n)) :
    Circuit Unbounded.signature n 1

    The circuit E_Q for a circuit C with one output: true at x exactly when C is true with the bits of Q set to true and false with the bits of Q set to false. For a monotone C, this says that C is undetermined at x by the bits outside Q (eval_undeterminedCircuit, Cslib.BitString.isUndetermined_iff_of_monotone). This construction is ours; compare the circuit of Chattopadhyay–Zuckerman, proof of Theorem 4.1.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.Braverman.eval_undeterminedCircuit {n : ℕ} (C : Circuit Unbounded.signature n 1) (Q : Finset (Fin n)) (x : BitString n) :
      (undeterminedCircuit C Q).eval Unbounded.interpretation x 0 = (C.eval Unbounded.interpretation (Q.piecewise (fun (x : Fin n) => true) x) 0 && !C.eval Unbounded.interpretation (Q.piecewise (fun (x : Fin n) => false) x) 0)

      E_Q computes C with Q set to true and not C with Q set to false.

      source
      @[simp]
      theorem Cslib.Circuits.Boolean.Braverman.size_undeterminedCircuit {n : ℕ} (C : Circuit Unbounded.signature n 1) (Q : Finset (Fin n)) :
      (undeterminedCircuit C Q).size = 2 * C.size + 6

      The size of E_Q, our count: exactly 2 m + 6 gates for a circuit C of m gates.

      source
      theorem Cslib.Circuits.Boolean.Braverman.depth_undeterminedCircuit_le {n : ℕ} (C : Circuit Unbounded.signature n 1) (Q : Finset (Fin n)) :
      (undeterminedCircuit C Q).depth ≤ C.depth + 3

      The depth of E_Q, our count: at most d + 3 for a circuit C of depth d.

      source
      theorem Cslib.Circuits.Boolean.Braverman.fanInAtMost_undeterminedCircuit {n : ℕ} {C : Circuit Unbounded.signature n 1} {r : ℕ} (hC : C.FanInAtMost r) (Q : Finset (Fin n)) :
      (undeterminedCircuit C Q).FanInAtMost (max r 2)

      The fan-in of E_Q: at most max r 2 for a circuit C of fan-in at most r.

      Theorem 4.1 of Chattopadhyay and Zuckerman #

      source
      theorem Cslib.Circuits.Boolean.Braverman.coalitionInfluence_le_of_independence_le {n : ℕ} {D : PMF (BitString n)} {d p t : ℕ} {ε₂ : ℝ} (hp : 2 ≤ p) (C : Circuit Unbounded.signature n 1) (hmono : Monotone fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0) (hfan : C.FanInAtMost (2 ^ p - 1)) (hsize : 2 * C.size + 6 ≤ 2 ^ p) (hd : C.depth ≤ d) (Q : Finset (Fin n)) (hQ : (BitString.coalitionInfluence (Probability.PMF.uniformOfFintype (BitString n)) Q fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0) ≤ ε₂) (ht : independence (d + 3) p ≤ t) (hD : BitString.IsKWiseIndependent t D) :
      (BitString.coalitionInfluence D Q fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0) ≤ ε₂ + 1 / 2 ^ p

      Coalition influence under polylogarithmic independence, with the exact independence function independence Chattopadhyay–Zuckerman, Theorem 4.1, influence part. Let C be a circuit of the unbounded fan-in basis computing a monotone function f, of depth at most d, with 2 size C + 6 ≤ 2 ^ p and fan-in less than 2 ^ p, where p ≥ 2. If a coalition Q has influence at most ε₂ on f under the uniform distribution, then it has influence at most ε₂ + 2 ^ (-p) under every independence (d + 3) p-wise independent distribution.

      The size and depth conditions are those of Braverman's theorem for our circuit E_Q (undeterminedCircuit); the theorem is stated for one coalition and one distribution.

      source
      theorem Cslib.Circuits.Boolean.Braverman.abs_sum_bitVal_sub_half_le_of_independence_le {n : ℕ} {D : PMF (BitString n)} {d p t : ℕ} {ε₁ : ℝ} (hp : 1 ≤ p) (C : Circuit Unbounded.signature n 1) (hfan : C.FanInAtMost (2 ^ p - 1)) (hsize : C.size ≤ 2 ^ p) (hd : C.depth ≤ d) (hbias : |(Finset.univ.expect fun (x : Fin n → Bool) => BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)) - 1 / 2| ≤ ε₁) (ht : independence d p ≤ t) (hD : BitString.IsKWiseIndependent t D) :
      |∑ x : BitString n, (D x).toReal * BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0) - 1 / 2| ≤ ε₁ + 1 / 2 ^ p

      The bias under polylogarithmic independence, with the exact independence function independence Chattopadhyay–Zuckerman, Theorem 4.1, bias part. Let C be a circuit of the unbounded fan-in basis of depth at most d, with at most 2 ^ p gates and fan-in less than 2 ^ p, where p ≥ 1. If C is true with probability within ε₁ of 1 / 2 under the uniform distribution, then it is under every independence d p-wise independent distribution with error ε₁ + 2 ^ (-p). Monotonicity is not needed.

      source
      theorem Cslib.Circuits.Boolean.Braverman.abs_sum_bitVal_sub_half_le_of_isKWiseIndependent {n : ℕ} {D : PMF (BitString n)} {d p t : ℕ} {ε₁ : ℝ} (hp : 1 ≤ p) (C : Circuit Unbounded.signature n 1) (hfan : C.FanInAtMost (2 ^ p - 1)) (hsize : C.size ≤ 2 ^ p) (hd : C.depth ≤ d) (hbias : |(Finset.univ.expect fun (x : Fin n → Bool) => BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0)) - 1 / 2| ≤ ε₁) (ht : (64 * p) ^ ((2 * d + 3) * (d + 7) + 1) ≤ t) (hD : BitString.IsKWiseIndependent t D) :
      |∑ x : BitString n, (D x).toReal * BitString.bitVal ℝ (C.eval Unbounded.interpretation x 0) - 1 / 2| ≤ ε₁ + 1 / 2 ^ p

      The bias under polylogarithmic independence Chattopadhyay–Zuckerman, Theorem 4.1, bias part: the bias part with the closed-form independence (64 p) ^ ((2 d + 3) (d + 7) + 1) of independence_le.

      source
      theorem Cslib.Circuits.Boolean.Braverman.isKWiseResilient_of_isResilient {n d p q t : ℕ} {ε₂ : ℝ} (hp : 2 ≤ p) (C : Circuit Unbounded.signature n 1) (hmono : Monotone fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0) (hfan : C.FanInAtMost (2 ^ p - 1)) (hsize : 2 * C.size + 6 ≤ 2 ^ p) (hd : C.depth ≤ d) (hres : BitString.IsResilient q ε₂ fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0) (ht : (64 * p) ^ ((2 * d + 9) * (d + 10) + 1) ≤ t) :
      BitString.IsKWiseResilient t q (ε₂ + 1 / 2 ^ p) fun (x : Fin n → Bool) => C.eval Unbounded.interpretation x 0

      Resilient monotone AC⁰ functions are resilient under polylogarithmic independence Chattopadhyay–Zuckerman, Theorem 4.1, influence part. Let C be a circuit of the unbounded fan-in basis computing a monotone (q, ε₂)-resilient function, of depth at most d, with 2 size C + 6 ≤ 2 ^ p and fan-in less than 2 ^ p, where p ≥ 2. Then the function is t-independent (q, ε₂ + 2 ^ (-p))-resilient for every t ≥ (64 p) ^ ((2 d + 9) (d + 10) + 1).

      For a circuit of m gates and fan-in r, taking p ≥ max (log₂ (2 m + 6)) (max (log₂ (r + 1)) (log₂ (1 / ε))) this is t = (log (max m (r + 1) / ε)) ^ O(d²); the fan-in term is needed since the fan-in of this model is not bounded by the size. Chattopadhyay and Zuckerman have the exponent 3 d + 6, which is not claimed here: the exponent and constants are ours.