Randomized communication complexity of disjointness

Deciding whether Alice's and Bob's subsets of an n-element set are disjoint needs Ω(n) bits even with randomness and bounded error Kalyanasundaram and Schnitger. We follow Razborov's corruption argument [Raz92], Kushilevitz and Nisan, Chapter 4, with a variant of his distribution.

The hard distribution Disjointness.hardDist lives on pairs of subsets of 2 m + 1 points. It draws a uniformly random partition (i, Tx, Ty) of the points into a point and two sets of m points (Disjointness.parts) and uniformly random subsets x ⊆ Tx and y ⊆ Ty, and outputs the disjoint pair (x, y) or, with probability 1 / 2, the pair (x ∪ {i}, y ∪ {i}), which meets in exactly i. Razborov's distribution instead draws sets of size about n / 4 and gives the disjoint pairs probability 3 / 4. Given the partition, the two sets are independent, so on a rectangle A × B the disjoint pairs have mass the average of a₀ b₀ over the partitions, where a₀ and b₀ are the fractions of the subsets of Tx in A and of Ty in B, and the intersecting pairs have mass the average of a₁ b₁, where a₁ and b₁ are the fractions of the subsets of Tx ∪ {i} containing i in A and of Ty ∪ {i} in B. Call the partition bad for A if a₁ < a₀ / 3. Once Ty is fixed, i is a uniformly random point outside Ty and b₀ is fixed, and a family of subsets of the complement of Ty for which many points are bad is small (Finset.four_mul_sum_card_filter_notMem_le, proved by Markov's inequality and counting subsets of a cube). So the partitions bad for A or, symmetrically, for B carry at most half of the mass of the disjoint pairs, up to an exponentially small error, while on the others a₁ b₁ ≥ a₀ b₀ / 9. This is Razborov's corruption lemma (Disjointness.corrupted_hardDist): on every rectangle the intersecting pairs carry at least 1 / 18 of the mass of the disjoint pairs, up to (27 / 32) ^ r / 2 when 48 r ≤ m + 1.

By the corruption bound (Corrupted.mul_sub_le_of_ecomplexityFun_le), public-coin protocols with error 1 / 64 send at least ((m + 1) / 48 - 29) / 5 bits (PublicCoin.div_le_mul_ecomplexityFun_disjoint_add). Embedding the points into the positions of n-bit strings gives n ≤ 2 ^ 9 R + 2 ^ 12 for the public-coin complexity R of disjointness with error ε ≤ 1 / 64 (PublicCoin.le_mul_ecomplexityFun_disjointness_add_of_le), and majority votes of 72 runs (PublicCoin.ecomplexityFun_le_two_mul_mul_one_third) give n ≤ 2 ^ 16 R + 2 ^ 12 with error 1 / 3, for public coins (PublicCoin.le_mul_ecomplexityFun_disjointness_add) and private coins (PrivateCoin.le_mul_ecomplexityFun_disjointness_add). The constants are not optimized.

Main definitions

• Cslib.Communication.Disjointness.parts: the partitions of the points.
• Cslib.Communication.Disjointness.hardDist: the hard distribution.

Main results

• Cslib.Communication.Disjointness.corrupted_hardDist: Razborov's corruption lemma.
• Cslib.Communication.PublicCoin.div_le_mul_ecomplexityFun_disjoint_add: the public-coin lower bound for subsets of 2 m + 1 points.
• Cslib.Communication.PublicCoin.le_mul_ecomplexityFun_disjointness_add_of_le, Cslib.Communication.PublicCoin.le_mul_ecomplexityFun_disjointness_add, Cslib.Communication.PrivateCoin.le_mul_ecomplexityFun_disjointness_add: disjointness of n bits needs Ω(n) bits with bounded error.

References

• B. Kalyanasundaram and G. Schnitger, The probabilistic communication complexity of set intersection
• A. A. Razborov, On the distributional complexity of disjointness
• E. Kushilevitz and N. Nisan, Communication Complexity

Partitions of the points

def Cslib.Communication.Disjointness.parts (U : Type u_1) [DecidableEq U] [Fintype U] (m : ℕ) : Finset (U × Finset U × Finset U)

The triples (i, Tx, Ty) of a point i and two disjoint sets Tx, Ty of m points that avoid it. When there are 2 m + 1 points, these are the ordered partitions of the points into parts of sizes 1, m and m.

theorem Cslib.Communication.Disjointness.mem_parts {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} {T : U × Finset U × Finset U} : T ∈ parts U m ↔ T.1 ∉ T.2.1 ∧ T.1 ∉ T.2.2 ∧ Disjoint T.2.1 T.2.2 ∧ T.2.1.card = m ∧ T.2.2.card = m

Membership in parts.

theorem Cslib.Communication.Disjointness.compl_insert_eq_of_mem_parts {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) {T : U × Finset U × Finset U} (hT : T ∈ parts U m) : (insert T.1 T.2.2)ᶜ = T.2.1

In a partition (i, Tx, Ty) of 2 m + 1 points, Tx is the complement of Ty and i.

theorem Cslib.Communication.Disjointness.sum_parts {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) {M : Type u_2} [AddCommMonoid M] (F : U × Finset U × Finset U → M) : ∑ T ∈ parts U m, F T = ∑ Ty ∈ Finset.powersetCard m Finset.univ, ∑ i ∈ Tyᶜ, F (i, (insert i Ty)ᶜ, Ty)

Summing over the partitions (i, Tx, Ty) of 2 m + 1 points is summing over the sets Ty of m points and the points i outside them.

theorem Cslib.Communication.Disjointness.sum_parts_swap {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} {M : Type u_2} [AddCommMonoid M] (F : U × Finset U × Finset U → M) : ∑ T ∈ parts U m, F T = ∑ T ∈ parts U m, F (T.1, T.2.2, T.2.1)

Exchanging the two sets of a partition.

theorem Cslib.Communication.Disjointness.card_parts {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) : (parts U m).card = (Finset.powersetCard m Finset.univ).card * (m + 1)

There are (m + 1) C(2 m + 1, m) partitions: a set Ty of m points and one of the m + 1 points outside it.

theorem Cslib.Communication.Disjointness.card_parts_pos {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) : 0 < (parts U m).card

There is a partition.

The corruption inequality over partitions

The hard distribution

noncomputable def Cslib.Communication.Disjointness.hardWeight {U : Type u_1} [DecidableEq U] [Fintype U] (m : ℕ) (q : Finset U × Finset U) : ℝ

The mass of a pair of sets under hardDist: the probability that a uniformly random partition (i, Tx, Ty) from parts and a fair coin produce it, where on heads the pair is a uniformly random pair of subsets of Tx and Ty, and on tails it is such a pair with i added to both sets.

theorem Cslib.Communication.Disjointness.hardWeight_nonneg {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (q : Finset U × Finset U) : 0 ≤ hardWeight m q

The weights are nonnegative.

theorem Cslib.Communication.Disjointness.sum_hardWeight {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) : ∑ q : Finset U × Finset U, hardWeight m q = 1

The weights add up to one, so they form a distribution (hardDist).

noncomputable def Cslib.Communication.Disjointness.hardDist {U : Type u_1} [DecidableEq U] [Fintype U] (m : ℕ) (hU : Fintype.card U = 2 * m + 1) : PMF (Finset U × Finset U)

A hard distribution for disjointness, a variant of Razborov's distribution [Raz92] on pairs of subsets of 2 m + 1 points. Draw a uniformly random partition (i, Tx, Ty) of the points into a point and two sets of m points, and uniformly random subsets x ⊆ Tx and y ⊆ Ty; with probability 1 / 2 output the disjoint pair (x, y), and otherwise the pair (x ∪ {i}, y ∪ {i}), which meets in exactly i. Razborov draws subsets of fixed size m / 2 instead; drawing all subsets lets the corruption bound be proved by counting subsets of a cube (Finset.four_mul_sum_card_filter_notMem_le).

theorem Cslib.Communication.Disjointness.hardDist_apply_toReal {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) (q : Finset U × Finset U) : ((hardDist m hU) q).toReal = hardWeight m q

The masses of hardDist are the weights hardWeight.

theorem Cslib.Communication.Disjointness.hardDist_toOuterMeasure_disjoint {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) : ((hardDist m hU).toOuterMeasure {q : Finset U × Finset U | decide (Disjoint q.1 q.2) = true}).toReal = 1 / 2

Under hardDist, the sets are disjoint with probability 1 / 2.

theorem Cslib.Communication.Disjointness.corrupted_hardDist {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) {r : ℕ} (hr : 48 * r ≤ m + 1) : Corrupted (hardDist m hU) (fun (x y : Finset U) => decide (Disjoint x y)) true (1 / 18) ((27 / 32) ^ r / 2)

Razborov's corruption lemma for hardDist [Raz92]: on every rectangle A × B of pairs of subsets of 2 m + 1 points, the intersecting pairs carry at least 1 / 18 of the mass of the disjoint pairs, up to (27 / 32) ^ r / 2 whenever 48 r ≤ m + 1.

Randomized lower bounds

theorem Cslib.Communication.PublicCoin.div_le_mul_ecomplexityFun_disjoint_add {U : Type u_1} [DecidableEq U] [Fintype U] {m : ℕ} (hU : Fintype.card U = 2 * m + 1) : ↑((m + 1) / 48) ≤ (5 * ecomplexityFun (1 / 64) fun (x y : Finset U) => decide (Disjoint x y)) + 29

Disjointness needs Ω(m) bits with public coins, for subsets of 2 m + 1 points: a public-coin protocol deciding whether two such subsets are disjoint with error 1 / 64 sends at least ((m + 1) / 48 - 29) / 5 bits.

theorem Cslib.Communication.PublicCoin.le_mul_ecomplexityFun_disjointness_add_of_le {ε : ℝ} (hε : ε ≤ 1 / 64) (n : ℕ) : ↑n ≤ 2 ^ 9 * ecomplexityFun ε disjointness + 2 ^ 12

Disjointness needs Ω(n) bits with public coins and small error [Raz92], Kalyanasundaram and Schnitger: a public-coin protocol deciding whether two n-bit strings have disjoint supports with error ε ≤ 1 / 64 sends at least (n - 2 ^ 12) / 2 ^ 9 bits.

theorem Cslib.Communication.PublicCoin.le_mul_ecomplexityFun_disjointness_add (n : ℕ) : ↑n ≤ 2 ^ 16 * ecomplexityFun (1 / 3) disjointness + 2 ^ 12

Disjointness needs Ω(n) bits with public coins Kalyanasundaram and Schnitger, [Raz92]: a public-coin protocol deciding whether two n-bit strings have disjoint supports with error 1 / 3 sends at least (n - 2 ^ 12) / 2 ^ 16 bits. Majority votes of 72 runs reduce the error to (8 / 9) ^ 36 ≤ 1 / 64 (PublicCoin.ecomplexityFun_le_two_mul_mul_one_third).

theorem Cslib.Communication.PrivateCoin.le_mul_ecomplexityFun_disjointness_add (n : ℕ) : ↑n ≤ 2 ^ 16 * ecomplexityFun (1 / 3) disjointness + 2 ^ 12

Disjointness needs Ω(n) bits with private coins Kalyanasundaram and Schnitger, [Raz92]: a private-coin protocol deciding whether two n-bit strings have disjoint supports with error 1 / 3 sends at least (n - 2 ^ 12) / 2 ^ 16 bits.