@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.map {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (g : α → β) (p : Protocol Ω_X Ω_Y X Y α) : Protocol Ω_X Ω_Y X Y β

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

Equations

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

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.map_rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (g : α → β) (p : Protocol Ω_X Ω_Y X Y α) (x : X) (y : Y) (ω_x : Ω_X) (ω_y : Ω_Y) : (map g p).rrun x y ω_x ω_y = g (p.rrun x y ω_x ω_y)

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.map_complexity {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (g : α → β) (p : Protocol Ω_X Ω_Y X Y α) : Deterministic.FiniteMessage.Protocol.complexity (map g p) = Deterministic.FiniteMessage.Protocol.complexity p

@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.bind {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (p : Protocol Ω_X Ω_Y X Y α) (q : α → Protocol Ω_X Ω_Y X Y β) : Protocol Ω_X Ω_Y 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.PrivateCoin.FiniteMessage.Protocol.bind_rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (p : Protocol Ω_X Ω_Y X Y α) (q : α → Protocol Ω_X Ω_Y X Y β) (x : X) (y : Y) (ω_x : Ω_X) (ω_y : Ω_Y) : (p.bind q).rrun x y ω_x ω_y = (q (p.rrun x y ω_x ω_y)).rrun x y ω_x ω_y

@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.comapRandomness {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} (hX : Ω_X' → Ω_X) (hY : Ω_Y' → Ω_Y) (p : Protocol Ω_X Ω_Y X Y α) : Protocol Ω_X' Ω_Y' X Y α

Reindex both randomness spaces of a private-coin protocol.

Equations

• CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.comapRandomness hX hY p = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap p (Prod.map hX id) (Prod.map hY id)

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.comapRandomness_rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} (hX : Ω_X' → Ω_X) (hY : Ω_Y' → Ω_Y) (p : Protocol Ω_X Ω_Y X Y α) (x : X) (y : Y) (ω_x : Ω_X') (ω_y : Ω_Y') : (comapRandomness hX hY p).rrun x y ω_x ω_y = p.rrun x y (hX ω_x) (hY ω_y)

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.comapRandomness_complexity {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} (hX : Ω_X' → Ω_X) (hY : Ω_Y' → Ω_Y) (p : Protocol Ω_X Ω_Y X Y α) : Deterministic.FiniteMessage.Protocol.complexity (comapRandomness hX hY p) = Deterministic.FiniteMessage.Protocol.complexity p

@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.prod {Ω_X1 : Type u_5} {Ω_X2 : Type u_6} {Ω_Y1 : Type u_7} {Ω_Y2 : Type u_8} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X1 Ω_Y1 X Y α₁) (p2 : Protocol Ω_X2 Ω_Y2 X Y α₂) : Protocol (Ω_X1 × Ω_X2) (Ω_Y1 × Ω_Y2) X Y (α₁ × α₂)

Product of two private-coin protocols with different randomness spaces. The result uses Ω_X1 × Ω_X2 and Ω_Y1 × Ω_Y2.

Equations

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

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.prod_rrun {Ω_X1 : Type u_5} {Ω_X2 : Type u_6} {Ω_Y1 : Type u_7} {Ω_Y2 : Type u_8} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X1 Ω_Y1 X Y α₁) (p2 : Protocol Ω_X2 Ω_Y2 X Y α₂) (x : X) (y : Y) (ω_x : Ω_X1 × Ω_X2) (ω_y : Ω_Y1 × Ω_Y2) : (p1.prod p2).rrun x y ω_x ω_y = (p1.rrun x y ω_x.1 ω_y.1, p2.rrun x y ω_x.2 ω_y.2)

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.prod_complexity {Ω_X1 : Type u_5} {Ω_X2 : Type u_6} {Ω_Y1 : Type u_7} {Ω_Y2 : Type u_8} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X1 Ω_Y1 X Y α₁) (p2 : Protocol Ω_X2 Ω_Y2 X Y α₂) : Deterministic.FiniteMessage.Protocol.complexity (p1.prod p2) = Deterministic.FiniteMessage.Protocol.complexity p1 + Deterministic.FiniteMessage.Protocol.complexity p2

@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.pi {X : Type u_9} {Y : Type u_10} {k : ℕ} {Ω_Xf : Fin k → Type u_15} {Ω_Yf : Fin k → Type u_16} {αf : Fin k → Type u_17} (p : (i : Fin k) → Protocol (Ω_Xf i) (Ω_Yf i) X Y (αf i)) : Protocol ((i : Fin k) → Ω_Xf i) ((i : Fin k) → Ω_Yf i) X Y ((i : Fin k) → αf i)

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

Equations

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

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.pi_rrun {X : Type u_9} {Y : Type u_10} {k : ℕ} {Ω_Xf : Fin k → Type u_15} {Ω_Yf : Fin k → Type u_16} {αf : Fin k → Type u_17} (p : (i : Fin k) → Protocol (Ω_Xf i) (Ω_Yf i) X Y (αf i)) (x : X) (y : Y) (ω_x : (i : Fin k) → Ω_Xf i) (ω_y : (i : Fin k) → Ω_Yf i) : (pi p).rrun x y ω_x ω_y = fun (i : Fin k) => (p i).rrun x y (ω_x i) (ω_y i)

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.pi_complexity {X : Type u_9} {Y : Type u_10} {k : ℕ} {Ω_Xf : Fin k → Type u_15} {Ω_Yf : Fin k → Type u_16} {αf : Fin k → Type u_17} (p : (i : Fin k) → Protocol (Ω_Xf i) (Ω_Yf i) X Y (αf i)) : Deterministic.FiniteMessage.Protocol.complexity (pi p) = ∑ i : Fin k, Deterministic.FiniteMessage.Protocol.complexity (p i)

@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.rbind {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (p : Protocol Ω_X Ω_Y X Y α) (q : α → Protocol Ω_X' Ω_Y' X Y β) : Protocol (Ω_X × Ω_X') (Ω_Y × Ω_Y') X Y β

Bind with fresh randomness: runs p with randomness Ω_X, Ω_Y, then q with independent randomness Ω_X', Ω_Y'.

Equations

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

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.rbind_rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (p : Protocol Ω_X Ω_Y X Y α) (q : α → Protocol Ω_X' Ω_Y' X Y β) (x : X) (y : Y) (ω_x : Ω_X × Ω_X') (ω_y : Ω_Y × Ω_Y') : (p.rbind q).rrun x y ω_x ω_y = (q (p.rrun x y ω_x.1 ω_y.1)).rrun x y ω_x.2 ω_y.2

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.rbind_complexity_const {Ω_X : Type u_1} {Ω_Y : Type u_2} {Ω_X' : Type u_3} {Ω_Y' : Type u_4} {X : Type u_9} {Y : Type u_10} {α : Type u_11} {β : Type u_14} (p : Protocol Ω_X Ω_Y X Y α) (q : α → Protocol Ω_X' Ω_Y' 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.PrivateCoin.FiniteMessage.Protocol.prodDet {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X Ω_Y X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) : Protocol Ω_X Ω_Y X Y (α₁ × α₂)

Product of a private-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.PrivateCoin.FiniteMessage.Protocol.prodDet_rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X Ω_Y X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) (x : X) (y : Y) (ω_x : Ω_X) (ω_y : Ω_Y) : (p1.prodDet p2).rrun x y ω_x ω_y = (p1.rrun x y ω_x ω_y, p2.run x y)

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.prodDet_complexity {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_9} {Y : Type u_10} {α₁ : Type u_12} {α₂ : Type u_13} (p1 : Protocol Ω_X Ω_Y X Y α₁) (p2 : Deterministic.FiniteMessage.Protocol X Y α₂) : Deterministic.FiniteMessage.Protocol.complexity (p1.prodDet p2) = Deterministic.FiniteMessage.Protocol.complexity p1 + p2.complexity