Coalition influence and resilient functions

A Boolean function f on the cube ι → Bool is undetermined at x by the bits outside a coalition Q (Cslib.BitString.IsUndetermined) if two strings that agree with x outside Q take different values: after the bits outside Q are fixed to those of x, the coalition can still decide the outcome. The influence of Q under a distribution D (Cslib.BitString.coalitionInfluence) is the probability, for x drawn from D, that f is undetermined at x by the bits outside Q. Under the uniform distribution this is the influence I_Q(f) of Chattopadhyay–Zuckerman, Definition 1.6, which is the coalitional influence of O'Donnell, Exercise 9.25; under a distribution D it is the influence I_{Q,D}(f) of Chattopadhyay–Zuckerman, Definition 1.9.

Chattopadhyay and Zuckerman fix the bits outside Q by a distribution on those bits alone. Here D is a distribution on all of the cube and the event ignores the bits in Q (Cslib.BitString.isUndetermined_congr), so coalitionInfluence D Q f is their I_{Q,D'}(f) for the marginal D' of D outside Q. The marginal of a k-wise independent distribution is again k-wise independent, and a k-wise independent distribution outside Q extends by uniform bits on Q, so the worst case over k-wise independent distributions is the same in both readings; this equivalence is not formalized.

A function is (q, ε)-resilient (Cslib.BitString.IsResilient) if every coalition of q bits has influence at most ε under the uniform distribution Chattopadhyay–Zuckerman, Definition 1.7, and t-independent (q, ε)-resilient (Cslib.BitString.IsKWiseResilient) if this holds under every t-wise independent distribution Chattopadhyay–Zuckerman, Definition 1.10. Chattopadhyay and Zuckerman define the largest influence I_q(f) and I_{q,t}(f) and bound it by ε; the predicates state the bound for every coalition and distribution directly.

Equivalently, f is undetermined at x by the bits outside Q when its restriction fixing the bits outside Q to those of x is not constant (Cslib.BitString.isUndetermined_iff_outside).

For a monotone function, f is undetermined at x by the bits outside Q exactly when setting all of Q to true gives true and setting all of Q to false gives false (Cslib.BitString.isUndetermined_iff_of_monotone). The influence of a single bit is the influence of Cslib.BitString.influence (Cslib.BitString.coalitionInfluence_singleton) O'Donnell, Exercise 9.25(a).

Main definitions

• Cslib.BitString.IsUndetermined: f is undetermined at x by the bits outside Q.
• Cslib.BitString.coalitionInfluence: the influence of a coalition under a distribution.
• Cslib.BitString.IsResilient: (q, ε)-resilient functions.
• Cslib.BitString.IsKWiseResilient: t-independent (q, ε)-resilient functions.

Main results

• Cslib.BitString.isUndetermined_iff_outside: undetermined functions are those with a non-constant restriction.
• Cslib.BitString.isUndetermined_iff_of_monotone: undetermined monotone functions.
• Cslib.BitString.coalitionInfluence_uniformOfFintype: the uniform influence as an average.
• Cslib.BitString.coalitionInfluence_nonneg, Cslib.BitString.coalitionInfluence_le_one, Cslib.BitString.coalitionInfluence_mono: influences are probabilities, monotone in the coalition.
• Cslib.BitString.coalitionInfluence_singleton: the influence of a single bit.
• Cslib.BitString.isResilient_const: constant functions are resilient against every coalition.

References

• E. Chattopadhyay, D. Zuckerman, Explicit two-source extractors and resilient functions
• R. O'Donnell, Analysis of Boolean Functions

Undetermined functions

def Cslib.BitString.IsUndetermined {ι : Type u_1} (Q : Finset ι) (f : (ι → Bool) → Bool) (x : ι → Bool) : Prop

The function f is undetermined at x by the bits outside the coalition Q if two strings agreeing with x outside Q take different values under f Chattopadhyay–Zuckerman, Definitions 1.6 and 1.9.

theorem Cslib.BitString.isUndetermined_congr {ι : Type u_1} {Q : Finset ι} {f : (ι → Bool) → Bool} {x x' : ι → Bool} (h : ∀ i ∉ Q, x i = x' i) : IsUndetermined Q f x ↔ IsUndetermined Q f x'

Whether f is undetermined at x by the bits outside Q depends only on the bits of x outside Q.

theorem Cslib.BitString.IsUndetermined.mono {ι : Type u_1} {Q Q' : Finset ι} {f : (ι → Bool) → Bool} {x : ι → Bool} (h : IsUndetermined Q f x) (hQ : Q ⊆ Q') : IsUndetermined Q' f x

A larger coalition leaves the function undetermined wherever a smaller one does.

theorem Cslib.BitString.not_isUndetermined_const {ι : Type u_1} {Q : Finset ι} {x : ι → Bool} (b : Bool) : ¬IsUndetermined Q (fun (x : ι → Bool) => b) x

A constant function is undetermined nowhere.

theorem Cslib.BitString.isUndetermined_iff_outside {ι : Type u_1} {Q : Finset ι} {f : (ι → Bool) → Bool} {x : ι → Bool} [DecidableEq ι] : IsUndetermined Q f x ↔ ∃ (y : ι → Bool) (z : ι → Bool), f ((PartialAssignment.outside Q x).fill y) ≠ f ((PartialAssignment.outside Q x).fill z)

A function is undetermined at x by the bits outside Q exactly when its restriction fixing the bits outside Q to those of x (Cslib.BitString.PartialAssignment.outside) is not constant.

theorem Cslib.BitString.isUndetermined_iff_of_monotone {ι : Type u_1} {Q : Finset ι} {f : (ι → Bool) → Bool} {x : ι → Bool} [DecidableEq ι] (hf : Monotone f) : IsUndetermined Q f x ↔ f (Q.piecewise (fun (x : ι) => true) x) = true ∧ f (Q.piecewise (fun (x : ι) => false) x) = false

Undetermined monotone functions. A monotone function is undetermined at x by the bits outside Q exactly when setting all of Q to true gives true and setting all of Q to false gives false.

theorem Cslib.BitString.isUndetermined_singleton_iff {ι : Type u_1} {f : (ι → Bool) → Bool} {x : ι → Bool} [DecidableEq ι] (i : ι) : IsUndetermined {i} f x ↔ f (Function.update x i !x i) ≠ f x

A function is undetermined at x by the bits other than i exactly when flipping bit i of x changes its value.

Coalition influence

@[instance_reducible]

instance Cslib.BitString.instDecidablePredForallBoolIsUndetermined {ι : Type u_1} [DecidableEq ι] [Fintype ι] (Q : Finset ι) (f : (ι → Bool) → Bool) : DecidablePred (IsUndetermined Q f)

noncomputable def Cslib.BitString.coalitionInfluence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (Q : Finset ι) (f : (ι → Bool) → Bool) : ℝ

The influence of the coalition Q on f under the distribution D: the probability, for x drawn from D, that f is undetermined at x by the bits outside Q. This is I_{Q,D}(f) Chattopadhyay–Zuckerman, Definition 1.9 for the marginal of D outside Q; under the uniform distribution it is I_Q(f) Chattopadhyay–Zuckerman, Definition 1.6, the coalitional influence of O'Donnell, Exercise 9.25.

theorem Cslib.BitString.coalitionInfluence_uniformOfFintype {ι : Type u_1} [DecidableEq ι] [Fintype ι] (Q : Finset ι) (f : (ι → Bool) → Bool) : coalitionInfluence (Probability.PMF.uniformOfFintype (ι → Bool)) Q f = Finset.univ.expect fun (x : ι → Bool) => if IsUndetermined Q f x then 1 else 0

Under the uniform distribution, the influence of a coalition is the fraction of the strings at which the function is undetermined by the bits outside it.

theorem Cslib.BitString.coalitionInfluence_nonneg {ι : Type u_1} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (Q : Finset ι) (f : (ι → Bool) → Bool) : 0 ≤ coalitionInfluence D Q f

Influences are nonnegative O'Donnell, Exercise 9.25(b).

theorem Cslib.BitString.coalitionInfluence_le_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (Q : Finset ι) (f : (ι → Bool) → Bool) : coalitionInfluence D Q f ≤ 1

Influences are at most one O'Donnell, Exercise 9.25(b).

theorem Cslib.BitString.coalitionInfluence_mono {ι : Type u_1} {Q Q' : Finset ι} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (hQ : Q ⊆ Q') (f : (ι → Bool) → Bool) : coalitionInfluence D Q f ≤ coalitionInfluence D Q' f

A larger coalition has at least the influence of a smaller one.

theorem Cslib.BitString.coalitionInfluence_eq_one_of_forall {ι : Type u_1} {Q : Finset ι} {f : (ι → Bool) → Bool} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (h : ∀ (x : ι → Bool), IsUndetermined Q f x) : coalitionInfluence D Q f = 1

A coalition that leaves the function undetermined everywhere has influence one.

theorem Cslib.BitString.coalitionInfluence_eq_zero_of_forall_not {ι : Type u_1} {Q : Finset ι} {f : (ι → Bool) → Bool} [DecidableEq ι] [Fintype ι] (D : PMF (ι → Bool)) (h : ∀ (x : ι → Bool), ¬IsUndetermined Q f x) : coalitionInfluence D Q f = 0

A coalition that leaves the function determined everywhere has influence zero.

theorem Cslib.BitString.coalitionInfluence_singleton {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → Bool) : coalitionInfluence (Probability.PMF.uniformOfFintype (ι → Bool)) {i} f = influence i fun (x : ι → Bool) => signVal (f x)

The influence of a single bit under the uniform distribution is its influence Cslib.BitString.influence on the function read as signs, the probability that flipping it changes the value O'Donnell, Exercise 9.25(a).

Resilient functions

def Cslib.BitString.IsResilient {ι : Type u_1} [DecidableEq ι] [Fintype ι] (q : ℕ) (ε : ℝ) (f : (ι → Bool) → Bool) : Prop

A function is (q, ε)-resilient if every coalition of q bits has influence at most ε under the uniform distribution Chattopadhyay–Zuckerman, Definition 1.7. For q > card ι there is no such coalition and the predicate holds vacuously, while their largest influence I_q(f) is undefined.

def Cslib.BitString.IsKWiseResilient {ι : Type u_1} [DecidableEq ι] [Fintype ι] (t q : ℕ) (ε : ℝ) (f : (ι → Bool) → Bool) : Prop

A function is t-independent (q, ε)-resilient if every coalition of q bits has influence at most ε under every t-wise independent distribution Chattopadhyay–Zuckerman, Definition 1.10, with D a distribution on all bits. This is equivalent to their reading, with a distribution on the bits outside Q, by an argument not formalized here (see the module docstring). For q > card ι there is no coalition of q bits and the predicate holds vacuously, while their largest influence I_{q,t}(f) is undefined.

theorem Cslib.BitString.IsKWiseResilient.isResilient {ι : Type u_1} {f : (ι → Bool) → Bool} [DecidableEq ι] [Fintype ι] {t q : ℕ} {ε : ℝ} (h : IsKWiseResilient t q ε f) : IsResilient q ε f

A t-independent resilient function is resilient, since the uniform distribution is t-wise independent.

theorem Cslib.BitString.isKWiseResilient_const {ι : Type u_1} [DecidableEq ι] [Fintype ι] (t q : ℕ) (b : Bool) : IsKWiseResilient t q 0 fun (x : ι → Bool) => b

A constant function is t-independent (q, 0)-resilient for all t and q.

theorem Cslib.BitString.isResilient_const {ι : Type u_1} [DecidableEq ι] [Fintype ι] (q : ℕ) (b : Bool) : IsResilient q 0 fun (x : ι → Bool) => b

A constant function is (q, 0)-resilient for every q.