Documentation

Complexity.Computability.Circuit.Boolean.Tribes

Tribes under bounded independence #

The Tribes function Tribes_{w,s} (Cslib.BitString.tribes) is computed by a depth-two circuit of the unbounded fan-in basis, an OR of s ANDs of w inputs each (tribesCircuit), with s + 1 gates and fan-in max s w. Through Chattopadhyay–Zuckerman, Theorem 4.1 (Cslib.Circuits.Boolean.Braverman.isKWiseResilient_of_isResilient), the resilience of Tribes (Cslib.BitString.isResilient_tribes) and its near balance (Cslib.BitString.abs_expect_bitVal_tribes_sub_half_le) carry over, with an error 2 ^ (-p), to every t-wise independent distribution with t ≥ (64 p) ^ 157, where p ≥ 2, 2 s + 8 ≤ 2 ^ p and w < 2 ^ p; for the bias, t ≥ (64 p) ^ 64 suffices, where p ≥ 1 and s, w < 2 ^ p. These exponents are those of the library's form of Braverman's theorem at depths 5 and 2; they are ours, and Chattopadhyay and Zuckerman's exponent 3 d + 6 is not claimed.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.tribesCircuit (w s : ℕ) :
Circuit Unbounded.signature (s * w) 1

The depth-two circuit computing Tribes_{w,s}: the OR of the ANDs of the tribes.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Boolean.eval_tribesCircuit {w s : ℕ} (x : BitString (s * w)) :
    (tribesCircuit w s).eval Unbounded.interpretation x 0 = BitString.tribes w s x

    tribesCircuit w s computes Tribes_{w,s}.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.size_tribesCircuit {w s : ℕ} :
    (tribesCircuit w s).size = s + 1

    tribesCircuit w s has s + 1 gates.

    source
    theorem Cslib.Circuits.Boolean.depth_tribesCircuit_le {w s : ℕ} :
    (tribesCircuit w s).depth ≤ 2

    tribesCircuit w s has depth at most two.

    source
    theorem Cslib.Circuits.Boolean.fanInAtMost_tribesCircuit {w s : ℕ} :
    (tribesCircuit w s).FanInAtMost (max s w)

    tribesCircuit w s has fan-in at most max s w.

    source
    theorem Cslib.Circuits.Boolean.Braverman.isKWiseResilient_tribes {w s p q t : ℕ} (hp : 2 ≤ p) (hs : 2 * s + 8 ≤ 2 ^ p) (hw : w < 2 ^ p) (ht : (64 * p) ^ 157 ≤ t) :
    BitString.IsKWiseResilient t q (2 ^ q / 2 ^ w + 1 / 2 ^ p) (BitString.tribes w s)

    Tribes is resilient under bounded independence, our instance of Chattopadhyay–Zuckerman, Theorem 4.1: if p ≥ 2, 2 s + 8 ≤ 2 ^ p and w < 2 ^ p, then Tribes_{w,s} is t-independent (q, 2 ^ (q - w) + 2 ^ (-p))-resilient for every t ≥ (64 p) ^ 157. The exponent 157 is (2 d + 9) (d + 10) + 1 at the depth d = 2 of tribesCircuit.

    source
    theorem Cslib.Circuits.Boolean.Braverman.abs_sum_bitVal_tribes_sub_half_le {w s p t : ℕ} {D : PMF (BitString (s * w))} (hp : 1 ≤ p) (hs : s < 2 ^ p) (hw : w < 2 ^ p) (h₁ : 1 / 2 ≤ (1 - 2⁻¹ ^ w) ^ s) (h₂ : (1 - 2⁻¹ ^ w) ^ (s + 1) < 1 / 2) (ht : (64 * p) ^ 64 ≤ t) (hD : BitString.IsKWiseIndependent t D) :
    |∑ x : BitString (s * w), (D x).toReal * BitString.bitVal ℝ (BitString.tribes w s x) - 1 / 2| ≤ 2⁻¹ ^ w + 1 / 2 ^ p

    Tribes is nearly balanced under bounded independence, our instance of Chattopadhyay–Zuckerman, Theorem 4.1, bias part: if s is largest with (1 - 2 ^ (-w)) ^ s ≥ 1 / 2 O'Donnell, Definition 4.11, p ≥ 1 and s, w < 2 ^ p, then under every t-wise independent distribution with t ≥ (64 p) ^ 64, Tribes_{w,s} is true with probability within 2 ^ (-w) + 2 ^ (-p) of 1 / 2. The exponent 64 is (2 d + 3) (d + 7) + 1 at d = 2.