@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.map {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (g : α → β) (p : Protocol Ω X Y α) : Protocol Ω X Y β

Map a function over the output of a public-coin protocol.

Equations

• CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.map g p = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map g p

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.map_rrun {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (g : α → β) (p : Protocol Ω X Y α) (x : X) (y : Y) (ω : Ω) : (map g p).rrun x y ω = g (p.rrun x y ω)

@[simp]

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

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.bind {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (p : Protocol Ω X Y α) (q : α → Protocol Ω X Y β) : Protocol Ω X Y β

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

Equations

• p.bind q = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bind p q

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.bind_rrun {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (p : Protocol Ω X Y α) (q : α → Protocol Ω X Y β) (x : X) (y : Y) (ω : Ω) : (p.bind q).rrun x y ω = (q (p.rrun x y ω)).rrun x y ω

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.comapRandomness {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} (h : Ω' → Ω) (p : Protocol Ω X Y α) : Protocol Ω' X Y α

Reindex the randomness space of a public-coin protocol via h : Ω' → Ω.

Equations

• CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.comapRandomness h p = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap p (Prod.map h id) (Prod.map h id)

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.comapRandomness_rrun {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} (h : Ω' → Ω) (p : Protocol Ω X Y α) (x : X) (y : Y) (ω : Ω') : (comapRandomness h p).rrun x y ω = p.rrun x y (h ω)

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.comapRandomness_complexity {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} (h : Ω' → Ω) (p : Protocol Ω X Y α) : Deterministic.FiniteMessage.Protocol.complexity (comapRandomness h p) = Deterministic.FiniteMessage.Protocol.complexity p

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prod {Ω₁ : Type u_3} {Ω₂ : 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 Y (α₁ × α₂)

Product of two public-coin protocols with different randomness spaces. The result uses Ω₁ × Ω₂ as shared randomness.

Equations

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

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prod_rrun {Ω₁ : Type u_3} {Ω₂ : 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) (y : Y) (ω : Ω₁ × Ω₂) : (p1.prod p2).rrun x y ω = (p1.rrun x y ω.1, p2.rrun x y ω.2)

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prod_complexity {Ω₁ : Type u_3} {Ω₂ : 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 α₂) : Deterministic.FiniteMessage.Protocol.complexity (p1.prod p2) = Deterministic.FiniteMessage.Protocol.complexity p1 + Deterministic.FiniteMessage.Protocol.complexity p2

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.pi {X : Type u_5} {Y : Type u_6} {k : ℕ} {Ωf : Fin k → Type u_11} {αf : Fin k → Type u_12} (p : (i : Fin k) → Protocol (Ωf i) X Y (αf i)) : Protocol ((i : Fin k) → Ωf i) X Y ((i : Fin k) → αf i)

Pi (k-fold product) of public-coin protocols with heterogeneous randomness and output types.

Equations

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

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.pi_rrun {X : Type u_5} {Y : Type u_6} {k : ℕ} {Ωf : Fin k → Type u_11} {αf : Fin k → Type u_12} (p : (i : Fin k) → Protocol (Ωf i) X Y (αf i)) (x : X) (y : Y) (ω : (i : Fin k) → Ωf i) : (pi p).rrun x y ω = fun (i : Fin k) => (p i).rrun x y (ω i)

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.pi_complexity {X : Type u_5} {Y : Type u_6} {k : ℕ} {Ωf : Fin k → Type u_11} {αf : Fin k → Type u_12} (p : (i : Fin k) → Protocol (Ωf i) X Y (αf i)) : Deterministic.FiniteMessage.Protocol.complexity (pi p) = ∑ i : Fin k, Deterministic.FiniteMessage.Protocol.complexity (p i)

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.rbind {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (p : Protocol Ω X Y α) (q : α → Protocol Ω' X Y β) : Protocol (Ω × Ω') X Y β

Bind with fresh randomness: runs p with randomness Ω, then q with independent randomness Ω'. The combined randomness is Ω × Ω'.

Equations

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

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.rbind_rrun {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (p : Protocol Ω X Y α) (q : α → Protocol Ω' X Y β) (x : X) (y : Y) (ω : Ω × Ω') : (p.rbind q).rrun x y ω = (q (p.rrun x y ω.1)).rrun x y ω.2

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.rbind_complexity_const {Ω : Type u_1} {Ω' : Type u_2} {X : Type u_5} {Y : Type u_6} {α : Type u_7} {β : Type u_10} (p : Protocol Ω X Y α) (q : α → Protocol Ω' X Y β) (c : ℕ) (hc : ∀ (a : α), Deterministic.FiniteMessage.Protocol.complexity (q a) = c) : Deterministic.FiniteMessage.Protocol.complexity (p.rbind q) = Deterministic.FiniteMessage.Protocol.complexity p + c

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prodDet {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol Ω X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) : Protocol Ω X Y (α₁ × α₂)

Product of a public-coin protocol with a deterministic protocol. Runs both on the same inputs and pairs their outputs.

Equations

• p1.prodDet p2 = p1.bind fun (a1 : α₁) => CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map (fun (a2 : α₂) => (a1, a2)) (p2.comap Prod.snd Prod.snd)

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prodDet_rrun {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol Ω X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) (x : X) (y : Y) (ω : Ω) : (p1.prodDet p2).rrun x y ω = (p1.rrun x y ω, p2.run x y)

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.prodDet_complexity {Ω : Type u_1} {X : Type u_5} {Y : Type u_6} {α₁ : Type u_8} {α₂ : Type u_9} (p1 : Protocol Ω X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) : Deterministic.FiniteMessage.Protocol.complexity (p1.prodDet p2) = Deterministic.FiniteMessage.Protocol.complexity p1 + p2.complexity