Protocols partition the inputs into rectangles

A combinatorial rectangle is a product A ×ˢ B of a set A of Alice's inputs and a set B of Bob's inputs. The inputs on which a deterministic protocol reaches a given leaf form a rectangle: a bit sent by Alice splits only Alice's side, and a bit sent by Bob only Bob's side. Numbering the leaves from left to right, the protocol reaches leaf i on x and y exactly when x lies in Alice's side leafAlice i and y in Bob's side leafBob i (Protocol.leaf_eq_iff), and its output there is the label leafOutput i of the leaf (Protocol.run_eq_leafOutput). So a protocol sending d bits partitions X × Y into at most 2 ^ d rectangles on each of which its output is constant (Protocol.exists_rectangle_partition); some of them may be empty Kushilevitz and Nisan, Chapter 1. When the protocol solves a relation on A × B, the label of each leaf is a valid answer on the part of its rectangle inside A × B (Protocol.Solves.solves_leafOutput).

Sums over all pairs of inputs split into sums over the leaf rectangles (Protocol.sum_eq_sum_leaves); so if each leaf rectangle labelled z has weight at most K, the inputs on which the protocol answers z have weight at most K times the number of such leaves (Protocol.sum_filter_run_le_mul). A protocol computes f : X → Y → Z when its output is f, which is solving the relation f x y = z on all inputs (Protocol.solves_univ_iff). Counting leaves by their labels turns bounds on rectangles into lower bounds on protocols: if f is constantly z only on rectangles of weight at most K, the inputs where f is z have weight at most K times the number of leaves labelled z, for every protocol computing f (Protocol.sum_filter_le_mul). Counting every input once, |f⁻¹(z)| ≤ K · #{leaves labelled z} when f is constantly z only on rectangles with at most K entries (Protocol.card_filter_le_mul).

Main definitions

• Cslib.Communication.Protocol.leaf: the leaf a protocol reaches.
• Cslib.Communication.Protocol.leafOutput: the labels of the leaves.
• Cslib.Communication.Protocol.leafAlice, Cslib.Communication.Protocol.leafBob: the sides of the rectangles of the leaves.

Main results

• Cslib.Communication.Protocol.leaf_eq_iff: the inputs reaching a leaf form a rectangle.
• Cslib.Communication.Protocol.run_eq_leafOutput: the output is constant on each rectangle.
• Cslib.Communication.Protocol.exists_rectangle_partition: a protocol sending d bits partitions the inputs into at most 2 ^ d monochromatic rectangles.
• Cslib.Communication.Protocol.Solves.solves_leafOutput: leaf rectangles inside the inputs of a solved relation are monochromatic.
• Cslib.Communication.Protocol.sum_eq_sum_leaves: sums over the leaf rectangles.
• Cslib.Communication.Protocol.sum_filter_run_le_mul: weights of the leaves with a given label.
• Cslib.Communication.Protocol.sum_filter_le_mul: the weighted area bound.
• Cslib.Communication.Protocol.card_filter_le_mul: the area bound.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

def Cslib.Communication.Protocol.leaf {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : X → Y → Fin p.leaves

The leaf a protocol reaches when Alice holds x and Bob holds y, numbering the leaves from left to right.

def Cslib.Communication.Protocol.leafOutput {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : Fin p.leaves → Z

The label of each leaf, numbering the leaves from left to right.

def Cslib.Communication.Protocol.leafAlice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : Fin p.leaves → Set X

Alice's side of the rectangle of each leaf: the inputs of Alice consistent with the bits she sends on the path to the leaf.

def Cslib.Communication.Protocol.leafBob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : Fin p.leaves → Set Y

Bob's side of the rectangle of each leaf: the inputs of Bob consistent with the bits he sends on the path to the leaf.

@[simp]

theorem Cslib.Communication.Protocol.leaf_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) (x : X) (y : Y) : (output z).leaf x y = ⟨0, Nat.zero_lt_one⟩

@[simp]

theorem Cslib.Communication.Protocol.leaf_alice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (x : X) (y : Y) : (alice send p₀ p₁).leaf x y = bif send x then Fin.natAdd p₀.leaves (p₁.leaf x y) else Fin.castAdd p₁.leaves (p₀.leaf x y)

@[simp]

theorem Cslib.Communication.Protocol.leaf_bob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (x : X) (y : Y) : (bob send' p₀ p₁).leaf x y = bif send' y then Fin.natAdd p₀.leaves (p₁.leaf x y) else Fin.castAdd p₁.leaves (p₀.leaf x y)

@[simp]

theorem Cslib.Communication.Protocol.leafOutput_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) (i : Fin (output z).leaves) : (output z).leafOutput i = z

@[simp]

theorem Cslib.Communication.Protocol.leafOutput_alice_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (alice send p₀ p₁).leafOutput (Fin.castAdd p₁.leaves i) = p₀.leafOutput i

@[simp]

theorem Cslib.Communication.Protocol.leafOutput_alice_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (alice send p₀ p₁).leafOutput (Fin.natAdd p₀.leaves i) = p₁.leafOutput i

@[simp]

theorem Cslib.Communication.Protocol.leafOutput_bob_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (bob send' p₀ p₁).leafOutput (Fin.castAdd p₁.leaves i) = p₀.leafOutput i

@[simp]

theorem Cslib.Communication.Protocol.leafOutput_bob_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (bob send' p₀ p₁).leafOutput (Fin.natAdd p₀.leaves i) = p₁.leafOutput i

@[simp]

theorem Cslib.Communication.Protocol.leafAlice_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) (i : Fin (output z).leaves) : (output z).leafAlice i = Set.univ

@[simp]

theorem Cslib.Communication.Protocol.leafAlice_alice_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (alice send p₀ p₁).leafAlice (Fin.castAdd p₁.leaves i) = {x : X | send x = false} ∩ p₀.leafAlice i

@[simp]

theorem Cslib.Communication.Protocol.leafAlice_alice_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (alice send p₀ p₁).leafAlice (Fin.natAdd p₀.leaves i) = {x : X | send x = true} ∩ p₁.leafAlice i

@[simp]

theorem Cslib.Communication.Protocol.leafAlice_bob_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (bob send' p₀ p₁).leafAlice (Fin.castAdd p₁.leaves i) = p₀.leafAlice i

@[simp]

theorem Cslib.Communication.Protocol.leafAlice_bob_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (bob send' p₀ p₁).leafAlice (Fin.natAdd p₀.leaves i) = p₁.leafAlice i

@[simp]

theorem Cslib.Communication.Protocol.leafBob_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) (i : Fin (output z).leaves) : (output z).leafBob i = Set.univ

@[simp]

theorem Cslib.Communication.Protocol.leafBob_alice_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (alice send p₀ p₁).leafBob (Fin.castAdd p₁.leaves i) = p₀.leafBob i

@[simp]

theorem Cslib.Communication.Protocol.leafBob_alice_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (alice send p₀ p₁).leafBob (Fin.natAdd p₀.leaves i) = p₁.leafBob i

@[simp]

theorem Cslib.Communication.Protocol.leafBob_bob_castAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₀.leaves) : (bob send' p₀ p₁).leafBob (Fin.castAdd p₁.leaves i) = {y : Y | send' y = false} ∩ p₀.leafBob i

@[simp]

theorem Cslib.Communication.Protocol.leafBob_bob_natAdd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send' : Y → Bool) (p₀ p₁ : Protocol X Y Z) (i : Fin p₁.leaves) : (bob send' p₀ p₁).leafBob (Fin.natAdd p₀.leaves i) = {y : Y | send' y = true} ∩ p₁.leafBob i

theorem Cslib.Communication.Protocol.leaf_eq_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {x : X} {y : Y} {i : Fin p.leaves} : p.leaf x y = i ↔ x ∈ p.leafAlice i ∧ y ∈ p.leafBob i

The inputs reaching a leaf form a rectangle: the protocol reaches leaf i on x and y exactly when x is on Alice's side and y on Bob's side of its rectangle.

theorem Cslib.Communication.Protocol.mem_leafAlice_leaf {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {x : X} {y : Y} : x ∈ p.leafAlice (p.leaf x y)

theorem Cslib.Communication.Protocol.mem_leafBob_leaf {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {x : X} {y : Y} : y ∈ p.leafBob (p.leaf x y)

theorem Cslib.Communication.Protocol.run_eq_leafOutput_leaf {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) (x : X) (y : Y) : p.run x y = p.leafOutput (p.leaf x y)

The output of a protocol is the label of the leaf it reaches.

theorem Cslib.Communication.Protocol.run_eq_leafOutput {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {x : X} {y : Y} {i : Fin p.leaves} (hx : x ∈ p.leafAlice i) (hy : y ∈ p.leafBob i) : p.run x y = p.leafOutput i

The output is constant on each leaf rectangle.

theorem Cslib.Communication.Protocol.exists_rectangle_partition {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : ∃ (n : ℕ) (A : Fin n → Set X) (B : Fin n → Set Y) (z : Fin n → Z), n ≤ 2 ^ p.depth ∧ (∀ (x : X) (y : Y), ∃! i : Fin n, x ∈ A i ∧ y ∈ B i) ∧ ∀ (i : Fin n), ∀ x ∈ A i, ∀ y ∈ B i, p.run x y = z i

A protocol sending d bits partitions X × Y into at most 2 ^ d monochromatic rectangles: there are at most 2 ^ d rectangles A i ×ˢ B i, possibly empty, such that every pair of inputs lies in exactly one of them and the output of the protocol is constant on each.

theorem Cslib.Communication.Protocol.Solves.solves_leafOutput {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} (hp : p.Solves R A B) (i : Fin p.leaves) : Communication.Solves (fun (x : X) (x_1 : Y) => p.leafOutput i) R (A ∩ p.leafAlice i) (B ∩ p.leafBob i)

Leaf rectangles are monochromatic: if a protocol solves R on A × B, the label of each leaf is a valid answer on the part of the leaf's rectangle inside A × B.

Sums over leaf rectangles

theorem Cslib.Communication.Protocol.sum_eq_sum_leaves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] {M : Type u_4} [AddCommMonoid M] (p : Protocol X Y Z) (g : X → Y → M) : ∑ x : X, ∑ y : Y, g x y = ∑ i : Fin p.leaves, ∑ x : X with x ∈ p.leafAlice i, ∑ y : Y with y ∈ p.leafBob i, g x y

Sums over leaf rectangles. A sum over all pairs of inputs is the sum, over the leaves of a protocol, of the sums over their rectangles.

theorem Cslib.Communication.Protocol.sum_filter_run_le_mul {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] {M : Type u_4} [Semiring M] [PartialOrder M] [IsOrderedAddMonoid M] [DecidableEq Z] (p : Protocol X Y Z) (z : Z) (w : X → Y → M) {K : M} (hK : ∀ (i : Fin p.leaves), p.leafOutput i = z → ∑ x : X with x ∈ p.leafAlice i, ∑ y : Y with y ∈ p.leafBob i, w x y ≤ K) : ∑ q : X × Y with p.run q.1 q.2 = z, w q.1 q.2 ≤ ↑{i : Fin p.leaves | p.leafOutput i = z}.card * K

Weights of the leaves with a given label. If every leaf rectangle labelled z has weight at most K under w, the inputs on which the protocol answers z have weight at most K times the number of leaves labelled z. The weights take values in an ordered semiring such as ℕ or ℝ, and may be negative.

theorem Cslib.Communication.Protocol.sum_filter_le_mul {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} [Fintype X] [Fintype Y] {M : Type u_4} [Semiring M] [PartialOrder M] [IsOrderedAddMonoid M] [DecidableEq Z] {f : X → Y → Z} (hp : p.run = f) (z : Z) (w : X → Y → M) {K : M} (hK : ∀ (A : Finset X) (B : Finset Y), (∀ x ∈ A, ∀ y ∈ B, f x y = z) → ∑ x ∈ A, ∑ y ∈ B, w x y ≤ K) : ∑ q : X × Y with f q.1 q.2 = z, w q.1 q.2 ≤ ↑{i : Fin p.leaves | p.leafOutput i = z}.card * K

The weighted area bound. If f is constantly z only on rectangles of weight at most K under w, then for every protocol computing f the inputs where f is z have weight at most K times the number of leaves labelled z. The weights take values in an ordered semiring such as ℕ or ℝ, and may be negative.

theorem Cslib.Communication.Protocol.card_filter_le_mul {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} [Fintype X] [Fintype Y] [DecidableEq Z] {f : X → Y → Z} (hp : p.run = f) (z : Z) {K : ℕ} (hK : ∀ (A : Finset X) (B : Finset Y), (∀ x ∈ A, ∀ y ∈ B, f x y = z) → A.card * B.card ≤ K) : {q : X × Y | f q.1 q.2 = z}.card ≤ {i : Fin p.leaves | p.leafOutput i = z}.card * K

The area bound. If f is constantly z only on rectangles with at most K entries, every protocol computing f has at least |f⁻¹(z)| / K leaves labelled z.