Documentation

Complexity.Foundations.BooleanAnalysis.Tribes

The Tribes function #

The Tribes function Tribes_{w,s} (Cslib.BitString.tribes) on s * w bits is the OR of s ANDs of w bits each, on disjoint tribes of bits O'Donnell, Definition 2.7, introduced by Ben-Or and Linial. It is monotone (Cslib.BitString.monotone_tribes) and true with probability 1 - (1 - 2 ^ (-w)) ^ s (Cslib.BitString.expect_bitVal_tribes) O'Donnell, Fact 4.10.

O'Donnell takes s largest with this probability at most 1 / 2 O'Donnell, Definition 4.11. This s exists for every w (Cslib.BitString.tribesSize) and lies in [2 ^ (w - 1), 2 ^ w) for w ≥ 1 (Cslib.BitString.two_pow_sub_one_le_tribesSize, Cslib.BitString.tribesSize_lt_two_pow); these bounds are ours. For such s we show that the probability is within 2 ^ (-w) of 1 / 2 (Cslib.BitString.abs_expect_bitVal_tribes_sub_half_le); this explicit bound is ours. O'Donnell's asymptotic statements, that then 2 ^ w = (n / ln n) (1 + o(1)) for n = s w with bias 1 / 2 - O(log n / n) and that each bit has influence (ln n / n) (1 ± o(1)) O'Donnell, Propositions 4.12 and 4.13, are not formalized.

A coalition Q leaves Tribes undetermined only if some tribe meets Q and is all true outside Q. A union bound over these tribes bounds the influence of Q by 2 ^ (|Q| - w) (Cslib.BitString.coalitionInfluence_tribes_le), so Tribes is (q, 2 ^ (q - w))-resilient (Cslib.BitString.isResilient_tribes); the bound and its proof are ours. It is useful only for q < w, about log n. Bribing one tribe, about log n voters, forces Tribes to True O'Donnell, Section 9.6, and the largest coalitional influence toward True of at most log n bits is 1 / 2 + Θ(log n / n) O'Donnell, Exercise 9.25(g). In our terms, one whole tribe of w bits has influence (1 - 2 ^ (-w)) ^ (s - 1), about 1 / 2 for the s above. For s = tribesSize w, this whole-tribe coalition rules out an O(q log n / n) influence bound at q = w as w tends to infinity, where n = s * w. This computation and conclusion are ours and are not formalized.

Main definitions #

Main results #

References #

The function #

source
def Cslib.BitString.tribes (w s : ℕ) (x : BitString (s * w)) :
Bool

Tribes Tribes_{w,s} O'Donnell, Definition 2.7: on s * w bits, the OR of s ANDs of w bits each, the i-th bit of the j-th tribe being bit finProdFinEquiv (j, i). The value true is O'Donnell's True, which he writes -1.

Instances For
    source
    theorem Cslib.BitString.tribes_eq_true_iff {w s : ℕ} {x : BitString (s * w)} :
    tribes w s x = true ↔ ∃ (j : Fin s), ∀ (i : Fin w), x (finProdFinEquiv (j, i)) = true

    Tribes is true exactly when some tribe is all true.

    source
    theorem Cslib.BitString.monotone_tribes (w s : ℕ) :
    Monotone (tribes w s)

    Tribes is monotone.

    The probability of true #

    source
    theorem Cslib.BitString.expect_bitVal_tribes (w s : ℕ) :
    (Finset.univ.expect fun (x : BitString (s * w)) => bitVal ℝ (tribes w s x)) = 1 - (1 - 2⁻¹ ^ w) ^ s

    The probability that Tribes is true O'Donnell, Fact 4.10: Pr[Tribes_{w,s} = True] = 1 - (1 - 2 ^ (-w)) ^ s.

    The number of tribes #

    source
    noncomputable def Cslib.BitString.tribesSize (w : ℕ) :
    ℕ

    The number of tribes of width w in O'Donnell's Tribes_n O'Donnell, Definition 4.11: the largest s with (1 - 2 ^ (-w)) ^ s ≥ 1 / 2, that is, with Tribes_{w,s} true with probability at most 1 / 2 (expect_bitVal_tribes). It is the least s with (1 - 2 ^ (-w)) ^ (s + 1) < 1 / 2, which exists since the base is less than 1. O'Donnell defines it for w ≥ 1; for w = 0 it is 0.

    Instances For
      source
      theorem Cslib.BitString.one_div_two_le_pow_tribesSize (w : ℕ) :
      1 / 2 ≤ (1 - 2⁻¹ ^ w) ^ tribesSize w

      Tribes_{w, tribesSize w} is true with probability at most 1 / 2 (1 - (1 - 2 ^ (-w)) ^ s ≤ 1 / 2).

      source
      theorem Cslib.BitString.pow_tribesSize_add_one_lt_one_div_two (w : ℕ) :
      (1 - 2⁻¹ ^ w) ^ (tribesSize w + 1) < 1 / 2

      tribesSize w is largest: one more tribe makes Tribes true with probability more than 1 / 2.

      source
      theorem Cslib.BitString.tribesSize_lt_two_pow (w : ℕ) :
      tribesSize w < 2 ^ w

      tribesSize w < 2 ^ w, our bound.

      source
      theorem Cslib.BitString.two_pow_sub_one_le_tribesSize {w : ℕ} (hw : 1 ≤ w) :
      2 ^ (w - 1) ≤ tribesSize w

      2 ^ (w - 1) ≤ tribesSize w for w ≥ 1, our bound.

      source
      theorem Cslib.BitString.abs_expect_bitVal_tribes_sub_half_le {w s : ℕ} (h₁ : 1 / 2 ≤ (1 - 2⁻¹ ^ w) ^ s) (h₂ : (1 - 2⁻¹ ^ w) ^ (s + 1) < 1 / 2) :
      |(Finset.univ.expect fun (x : BitString (s * w)) => bitVal ℝ (tribes w s x)) - 1 / 2| ≤ 2⁻¹ ^ w

      Tribes is nearly balanced, our explicit form of O'Donnell, Proposition 4.12, last statement: if s is largest with (1 - 2 ^ (-w)) ^ s ≥ 1 / 2, that is, Tribes_{w,s} is true with probability at most 1 / 2 O'Donnell, Definition 4.11, then the probability is within 2 ^ (-w) of 1 / 2. The bound is ours; O'Donnell states 1 / 2 - O(log n / n) for n = s w.

      Coalitions #

      source
      theorem Cslib.BitString.coalitionInfluence_tribes_le {w s : ℕ} (Q : Finset (Fin (s * w))) :
      coalitionInfluence (Probability.PMF.uniformOfFintype (Fin (s * w) → Bool)) Q (tribes w s) ≤ 2 ^ Q.card / 2 ^ w

      The influence of a coalition on Tribes, our union bound: a coalition Q has influence at most 2 ^ (|Q| - w) on Tribes_{w,s}.

      source
      theorem Cslib.BitString.isResilient_tribes (w s q : ℕ) :
      IsResilient q (2 ^ q / 2 ^ w) (tribes w s)

      Tribes is resilient against small coalitions, our bound: Tribes_{w,s} is (q, 2 ^ (q - w))-resilient Chattopadhyay–Zuckerman, Definition 1.7. This is useful only for q < w. For s = tribesSize w, a whole-tribe coalition rules out an O(q log n / n) influence bound at q = w as w tends to infinity, where n = s * w. This asymptotic conclusion is not formalized here (compare O'Donnell, Section 9.6).