noncomputable def CommunicationComplexity.Functions.Disjointness.disjointness (n : ℕ) (X Y : Set (Fin n)) : Bool

The set disjointness function on subsets of [n].

Equations

• CommunicationComplexity.Functions.Disjointness.disjointness n X Y = decide (Disjoint X Y)

theorem CommunicationComplexity.Functions.Disjointness.disjointness_comm (n : ℕ) (X Y : Set (Fin n)) : disjointness n X Y = disjointness n Y X

Disjointness is symmetric in Alice's and Bob's inputs.

def CommunicationComplexity.Functions.Disjointness.foolingSet (n : ℕ) : Set (Set (Fin n) × Set (Fin n))

The candidate fooling set for disjointness: pairs (X, Xᶜ).

Equations

• CommunicationComplexity.Functions.Disjointness.foolingSet n = {p : Set (Fin n) × Set (Fin n) | p.2 = p.1ᶜ}

theorem CommunicationComplexity.Functions.Disjointness.foolingSet_isFoolingSet (n : ℕ) : Rectangle.IsFoolingSet (foolingSet n) (disjointness n)

Claim 1.21: the pairs (X, Xᶜ) form a fooling set for disjointness.

theorem CommunicationComplexity.Functions.Disjointness.foolingSet_card (n : ℕ) : (foolingSet n).ncard = 2 ^ n

The fooling set for disjointness has size 2^n.

theorem CommunicationComplexity.Functions.Disjointness.communicationComplexity_le (n : ℕ) : Deterministic.communicationComplexity (disjointness n) ≤ ↑n + 1

The deterministic communication complexity of disjointness is at most n + 1: Alice sends her set, and Bob sends one bit for the answer.

theorem CommunicationComplexity.Functions.Disjointness.le_communicationComplexity (n : ℕ) (hn : 1 ≤ n) : ↑(n + 1) ≤ Deterministic.communicationComplexity (disjointness n)

For n ≥ 1, disjointness on subsets of [n] has deterministic communication complexity at least n + 1.

theorem CommunicationComplexity.Functions.Disjointness.communicationComplexity_eq (n : ℕ) (hn : 1 ≤ n) : Deterministic.communicationComplexity (disjointness n) = ↑n + 1

For n ≥ 1, the deterministic communication complexity of disjointness on subsets of [n] is exactly n + 1.