Intersection and inclusion

Disjointness of n-bit strings, read as subsets of the n positions, needs n + 1 bits for 0 < n (ecomplexity_disjointness). Since negating the output does not change the communication complexity, so does intersection, deciding whether the two sets meet (ecomplexityFun_not_disjointness). Inclusion x ≤ y (pointwise, so that the set of positions where x is true lies in that of y) also needs n + 1 bits for 0 < n (ecomplexityFun_decide_le): in any partial order the diagonal pairs (x, x) form a fooling set for ≤ with value true, by antisymmetry (isFoolingSet_le) Kushilevitz and Nisan, Chapter 1.

Main results

• Cslib.Communication.ecomplexityFun_not_disjointness: intersection of n bits needs n + 1 bits.
• Cslib.Communication.ecomplexityFun_decide_le: inclusion of n bits needs n + 1 bits.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

theorem Cslib.Communication.ecomplexityFun_not_disjointness {n : ℕ} (hn : 0 < n) : (Protocol.ecomplexityFun fun (x y : BitString n) => !disjointness x y) = ↑n + 1

Intersection of n bits needs n + 1 bits, for 0 < n: deciding whether two subsets of n positions meet costs as much as disjointness.

theorem Cslib.Communication.ecomplexityFun_decide_le {n : ℕ} (hn : 0 < n) : (Protocol.ecomplexityFun fun (x y : BitString n) => decide (x ≤ y)) = ↑n + 1

Inclusion of n bits needs n + 1 bits, for 0 < n: deciding whether x ≤ y pointwise, that is, whether the set of positions where x is true lies in that of y.