@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.Protocol.toDeterministic {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) : Deterministic.Protocol X Y α

Fix the randomness of a binary public-coin protocol, producing a deterministic protocol with the same complexity (via comap).

Equations

• p.toDeterministic ω = CommunicationComplexity.Deterministic.Protocol.comap p (Prod.mk ω) (Prod.mk ω)

@[simp]

theorem CommunicationComplexity.PublicCoin.Protocol.toDeterministic_run {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) (x : X) (y : Y) : (p.toDeterministic ω).run x y = p.rrun x y ω

@[simp]

theorem CommunicationComplexity.PublicCoin.Protocol.toDeterministic_complexity {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) : (p.toDeterministic ω).complexity = Deterministic.Protocol.complexity p

@[reducible, inline]

abbrev CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toPrivateCoin {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Ω_X : Type u_4} {Ω_Y : Type u_5} (p : Protocol X Y α) : PrivateCoin.FiniteMessage.Protocol Ω_X Ω_Y X Y α

Convert a deterministic finite-message protocol to a private-coin finite-message protocol by ignoring both coin spaces (via comap).

Equations

• p.toPrivateCoin = p.comap Prod.snd Prod.snd

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toPrivateCoin_rrun {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Ω_X : Type u_4} {Ω_Y : Type u_5} (p : Protocol X Y α) (x : X) (y : Y) (ω_x : Ω_X) (ω_y : Ω_Y) : p.toPrivateCoin.rrun x y ω_x ω_y = p.run x y

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toPrivateCoin_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Ω_X : Type u_4} {Ω_Y : Type u_5} (p : Protocol X Y α) : complexity p.toPrivateCoin = p.complexity

@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toDeterministic {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) : Deterministic.FiniteMessage.Protocol X Y α

Fix the randomness of a public-coin finite-message protocol, producing a deterministic finite-message protocol with the same complexity (via comap).

Equations

• p.toDeterministic ω = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap p (Prod.mk ω) (Prod.mk ω)

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toDeterministic_run {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) (x : X) (y : Y) : (p.toDeterministic ω).run x y = p.rrun x y ω

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toDeterministic_complexity {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) : (p.toDeterministic ω).complexity = Deterministic.FiniteMessage.Protocol.complexity p

theorem CommunicationComplexity.PrivateCoin.communicationComplexity_le_deterministic {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (hε : 0 ≤ ε) : communicationComplexity f ε ≤ Deterministic.communicationComplexity f

Private-coin communication complexity is at most deterministic communication complexity (for any non-negative error).