Fooling sets

A fooling set for f : X → Y → Z with value z is a finite set S of pairs of inputs on which f is z, such that for any two distinct pairs (x₁, y₁) and (x₂, y₂) of S, f x₁ y₂ ≠ z or f x₂ y₁ ≠ z (IsFoolingSet) Kushilevitz and Nisan, Chapter 1. A rectangle on which f is constantly z contains at most one pair of S. So a protocol computing f has at least |S| leaves labelled z (IsFoolingSet.card_le), and at least one leaf more when f takes another value somewhere: then |S| < 2 ^ d for every protocol sending d bits (IsFoolingSet.card_lt_two_pow). In particular a fooling set of 2 ^ n pairs for a function that is not constantly z forces n + 1 bits (IsFoolingSet.succ_le_ecomplexity).

Main definitions

• Cslib.Communication.IsFoolingSet: fooling sets.

Main results

• Cslib.Communication.IsFoolingSet.card_le: a fooling set for value z is at most the number of leaves labelled z.
• Cslib.Communication.IsFoolingSet.card_lt_two_pow: the fooling-set bound.
• Cslib.Communication.IsFoolingSet.succ_le_ecomplexity: the fooling-set bound on communication complexity.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

def Cslib.Communication.IsFoolingSet {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X → Y → Z) (z : Z) (S : Finset (X × Y)) : Prop

A fooling set for f with value z: a finite set S of pairs of inputs on which f is z, such that two pairs (x₁, y₁) and (x₂, y₂) of S with f x₁ y₂ = z and f x₂ y₁ = z are equal.

theorem Cslib.Communication.IsFoolingSet.card_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {z : Z} {S : Finset (X × Y)} {p : Protocol X Y Z} [DecidableEq Z] (hS : IsFoolingSet f z S) (hp : p.run = f) : S.card ≤ {i : Fin p.leaves | p.leafOutput i = z}.card

A protocol computing f reaches distinct leaves labelled z on the pairs of a fooling set for f with value z.

theorem Cslib.Communication.IsFoolingSet.card_lt_two_pow {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {z : Z} {S : Finset (X × Y)} {p : Protocol X Y Z} (hS : IsFoolingSet f z S) (hp : p.run = f) (hz : ∃ (x : X) (y : Y), f x y ≠ z) : S.card < 2 ^ p.depth

The fooling-set bound. If f takes a value other than z, a fooling set for f with value z has fewer than 2 ^ d pairs, for every protocol computing f with d bits.

theorem Cslib.Communication.IsFoolingSet.succ_le_ecomplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {z : Z} {S : Finset (X × Y)} (hS : IsFoolingSet f z S) (hz : ∃ (x : X) (y : Y), f x y ≠ z) {n : ℕ} (hn : 2 ^ n ≤ S.card) : ↑n + 1 ≤ Protocol.ecomplexityFun f

The fooling-set bound on communication complexity. A fooling set of at least 2 ^ n pairs for a function f that is not constantly z forces n + 1 bits.