def CommunicationComplexity.Deterministic.Protocol.swapInputSet {X : Type u_1} {Y : Type u_2} (R : Set (X × Y)) : Set (Y × X)

Swap the two coordinates in a protocol leaf rectangle.

Equations

• CommunicationComplexity.Deterministic.Protocol.swapInputSet R = {yx : Y × X | (yx.2, yx.1) ∈ R}

@[simp]

theorem CommunicationComplexity.Deterministic.Protocol.mem_swapInputSet {X : Type u_1} {Y : Type u_2} (R : Set (X × Y)) (yx : Y × X) : yx ∈ swapInputSet R ↔ (yx.2, yx.1) ∈ R

@[simp]

theorem CommunicationComplexity.Deterministic.Protocol.swapInputSet_swapInputSet {X : Type u_1} {Y : Type u_2} (R : Set (X × Y)) : swapInputSet (swapInputSet R) = R

def CommunicationComplexity.Deterministic.Protocol.preimageInputSet {X : Type u_1} {Y : Type u_2} {X' : Type u_4} {Y' : Type u_5} (fX : X' → X) (fY : Y' → Y) (R : Set (X × Y)) : Set (X' × Y')

Pull a protocol input set back along maps on Alice's and Bob's inputs.

Equations

• CommunicationComplexity.Deterministic.Protocol.preimageInputSet fX fY R = {xy : X' × Y' | (fX xy.1, fY xy.2) ∈ R}

@[simp]

theorem CommunicationComplexity.Deterministic.Protocol.mem_preimageInputSet {X : Type u_1} {Y : Type u_2} {X' : Type u_4} {Y' : Type u_5} (fX : X' → X) (fY : Y' → Y) (R : Set (X × Y)) (xy : X' × Y') : xy ∈ preimageInputSet fX fY R ↔ (fX xy.1, fY xy.2) ∈ R

def CommunicationComplexity.Deterministic.Protocol.leafRectangles {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : Set (Set (X × Y))

The set of rectangles induced by protocol leaves over all inputs X × Y.

Equations

• p.leafRectangles = CommunicationComplexity.Deterministic.Protocol.leafRectanglesAux✝ p Set.univ Set.univ

theorem CommunicationComplexity.Deterministic.Protocol.swapInputSet_mem_leafRectangles_swap {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) {R : Set (X × Y)} (hR : R ∈ p.leafRectangles) : swapInputSet R ∈ p.swap.leafRectangles

Swapping Alice and Bob sends protocol leaf rectangles to protocol leaf rectangles.

theorem CommunicationComplexity.Deterministic.Protocol.preimageInputSet_mem_leafRectangles_comap {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) {R : Set (X × Y)} (fX : X' → X) (fY : Y' → Y) (hR : R ∈ p.leafRectangles) : preimageInputSet fX fY R ∈ (p.comap fX fY).leafRectangles

Pulling back along Protocol.comap sends protocol leaf rectangles to protocol leaf rectangles.

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_isRectangle {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (R : Set (X × Y)) (hR : R ∈ p.leafRectangles) : Rectangle.IsRectangle R

Every protocol leaf-rectangle is a genuine rectangle.

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_cover {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : ⋃₀ p.leafRectangles = Set.univ

The leaf rectangles of a protocol cover the whole input space.

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_disjoint {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (R S : Set (X × Y)) (hR : R ∈ p.leafRectangles) (hS : S ∈ p.leafRectangles) (hne : R ≠ S) : Disjoint R S

Distinct protocol leaf rectangles are disjoint.

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_mono {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (g : X → Y → α) (h_comp : p.Computes g) (R : Set (X × Y)) (hR : R ∈ p.leafRectangles) : Rectangle.IsMonochromatic R g

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_card {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.leafRectangles.ncard ≤ 2 ^ p.complexity

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_finite {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.leafRectangles.Finite

The set of protocol leaf rectangles is finite.

theorem CommunicationComplexity.Deterministic.Protocol.leafRectangles_isMonoPartition {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (g : X → Y → α) (h_comp : p.Computes g) : Rectangle.IsMonoPartition p.leafRectangles g

The leaf rectangles of a protocol computing g form a monochromatic rectangle partition.

theorem CommunicationComplexity.Deterministic.Protocol.rectangle_partition {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (g : X → Y → α) (h_comp : p.Computes g) : Rectangle.IsMonoPartition p.leafRectangles g ∧ p.leafRectangles.ncard ≤ 2 ^ p.complexity

Theorem 1.6: if π computes g, then X × Y is partitioned into at most 2^c monochromatic rectangles with respect to g.

theorem CommunicationComplexity.Deterministic.Protocol.reachesPath_isRectangle {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.SubprotocolPath p) : Rectangle.IsRectangle {xy : X × Y | reachesPath hsp xy.1 xy.2}

The input pairs that reach a fixed subprotocol path form a rectangle.

theorem CommunicationComplexity.Deterministic.Protocol.reaches_isRectangle {X : Type u_1} {Y : Type u_2} {α : Type u_3} {s p : Protocol X Y α} (hsp : s.IsSubprotocol p) : Rectangle.IsRectangle {xy : X × Y | reaches hsp xy.1 xy.2}

The input pairs that reach a chosen subprotocol witness form a rectangle.

theorem CommunicationComplexity.Deterministic.mono_partition_of_communicationComplexity_le {X : Type u_1} {Y : Type u_2} {α : Type u_3} (g : X → Y → α) (n : ℕ) (h : communicationComplexity g ≤ ↑n) : ∃ (Part : Set (Set (X × Y))), Rectangle.IsMonoPartition Part g ∧ Part.ncard ≤ 2 ^ n

If deterministic_communication_complexity g ≤ n, then there is a monochromatic rectangle partition of X × Y with at most 2^n rectangles.

theorem CommunicationComplexity.Deterministic.communicationComplexity_lower_bound {X : Type u_1} {Y : Type u_2} {α : Type u_3} (g : X → Y → α) (n : ℕ) (h : ∀ (Part : Set (Set (X × Y))), Rectangle.IsMonoPartition Part g → 2 ^ n < Part.ncard) : ↑(n + 1) ≤ communicationComplexity g

Rectangle lower-bound method: to prove CC(g) ≥ n + 1, it suffices to show every monochromatic rectangle partition of g has more than 2^n parts.

theorem CommunicationComplexity.Deterministic.foolingSet_ncard_le_pow_of_communicationComplexity_le {X : Type u_1} {Y : Type u_2} {α : Type u_3} (g : X → Y → α) (S : Set (X × Y)) (n : ℕ) (hS : Rectangle.IsFoolingSet S g) (h : communicationComplexity g ≤ ↑n) : S.ncard ≤ 2 ^ n

If the deterministic communication complexity of g is at most n, then every fooling set for g has size at most 2^n.

theorem CommunicationComplexity.Deterministic.foolingSet_lower_bound {X : Type u_1} {Y : Type u_2} {α : Type u_3} (g : X → Y → α) (S : Set (X × Y)) (hS : Rectangle.IsFoolingSet S g) : ↑(Nat.clog 2 S.ncard) ≤ communicationComplexity g

Fooling-set lower bound: the deterministic communication complexity of g is at least ⌈log₂ |S|⌉ for every fooling set S of g.