def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} (g : α → β) : Protocol X Y α → Protocol X Y β

Map a function over the output of a protocol.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map_run {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} (g : α → β) (p : Protocol X Y α) (x : X) (y : Y) : (map g p).run x y = g (p.run x y)

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} (g : α → β) (p : Protocol X Y α) : (map g p).complexity = p.complexity

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bind {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} : Protocol X Y α → (α → Protocol X Y β) → Protocol X Y β

Bind: replace each output a in p with q a.

Equations

• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output a).bind x✝ = x✝ a
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f P).bind x✝ = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f fun (b : β_1) => (P b).bind x✝
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f P).bind x✝ = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f fun (b : β_1) => (P b).bind x✝

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bind_run {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} (p : Protocol X Y α) (q : α → Protocol X Y β) (x : X) (y : Y) : (p.bind q).run x y = (q (p.run x y)).run x y

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bind_complexity_const {X : Type u_1} {Y : Type u_2} {α : Type u_7} {β : Type u_10} (p : Protocol X Y α) (q : α → Protocol X Y β) (c : ℕ) (hc : ∀ (a : α), (q a).complexity = c) : (p.bind q).complexity = p.complexity + c

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.prod {X₁ : Type u_3} {Y₁ : Type u_4} {X₂ : Type u_5} {Y₂ : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol X₁ Y₁ α₁) (p2 : Protocol X₂ Y₂ α₂) : Protocol (X₁ × X₂) (Y₁ × Y₂) (α₁ × α₂)

Product of two protocols with disjoint input types. Runs p1 on the first components (X₁, Y₁) and p2 on the second (X₂, Y₂), pairing the outputs.

Equations

• One or more equations did not get rendered due to their size.
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f P).prod p2 = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice (f ∘ Prod.fst) fun (b : β) => (P b).prod p2
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f P).prod p2 = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob (f ∘ Prod.fst) fun (b : β) => (P b).prod p2

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.prod_run {X₁ : Type u_3} {Y₁ : Type u_4} {X₂ : Type u_5} {Y₂ : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol X₁ Y₁ α₁) (p2 : Protocol X₂ Y₂ α₂) (x : X₁ × X₂) (y : Y₁ × Y₂) : (p1.prod p2).run x y = (p1.run x.1 y.1, p2.run x.2 y.2)

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.prod_complexity {X₁ : Type u_3} {Y₁ : Type u_4} {X₂ : Type u_5} {Y₂ : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol X₁ Y₁ α₁) (p2 : Protocol X₂ Y₂ α₂) : (p1.prod p2).complexity = p1.complexity + p2.complexity

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.pi {k : ℕ} {Xf : Fin k → Type u_14} {Yf : Fin k → Type u_15} {αf : Fin k → Type u_16} : ((i : Fin k) → Protocol (Xf i) (Yf i) (αf i)) → Protocol ((i : Fin k) → Xf i) ((i : Fin k) → Yf i) ((i : Fin k) → αf i)

Pi (k-fold product) of protocols with heterogeneous input/output types. Runs each p i on the i-th components, collecting outputs.

Equations

• One or more equations did not get rendered due to their size.
• CommunicationComplexity.Deterministic.FiniteMessage.Protocol.pi x_8 = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output fun (i : Fin 0) => i.elim0

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.pi_run {k : ℕ} {Xf : Fin k → Type u_11} {Yf : Fin k → Type u_12} {αf : Fin k → Type u_13} (p : (i : Fin k) → Protocol (Xf i) (Yf i) (αf i)) (x : (i : Fin k) → Xf i) (y : (i : Fin k) → Yf i) : (pi p).run x y = fun (i : Fin k) => (p i).run (x i) (y i)

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.pi_complexity {k : ℕ} {Xf : Fin k → Type u_11} {Yf : Fin k → Type u_12} {αf : Fin k → Type u_13} (p : (i : Fin k) → Protocol (Xf i) (Yf i) (αf i)) : (pi p).complexity = ∑ i : Fin k, (p i).complexity