@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.FiniteMessage.Protocol (Ω : Type u_1) (X : Type u_2) (Y : Type u_3) (α : Type u_4) : Type (max (max (max 1 u_2 u_1) u_3 u_1) u_4)

A public-coin finite-message protocol is a deterministic finite-message protocol where Alice's input is Ω × X and Bob's is Ω × Y.

Equations

• CommunicationComplexity.PublicCoin.FiniteMessage.Protocol Ω X Y α = CommunicationComplexity.Deterministic.FiniteMessage.Protocol (Ω × X) (Ω × Y) α

def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.output {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (a : α) : Protocol Ω X Y α

Output node for a public-coin finite-message protocol.

Equations

• CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.output a = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output a

def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.alice {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} {β : Type} [Fintype β] [Nonempty β] (f : X → Ω → β) (P : β → Protocol Ω X Y α) : Protocol Ω X Y α

Alice sends a β-valued message depending on her input x and shared randomness ω.

Equations

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

def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.bob {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} {β : Type} [Fintype β] [Nonempty β] (f : Y → Ω → β) (P : β → Protocol Ω X Y α) : Protocol Ω X Y α

Bob sends a β-valued message depending on his input y and shared randomness ω.

Equations

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

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

Execute a public-coin finite-message protocol on inputs x, y with shared randomness ω.

Equations

• p.rrun x y ω = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.run p (ω, x) (ω, y)

@[simp]

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

def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.ApproxSatisfies {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} [MeasureTheory.MeasureSpace Ω] (p : Protocol Ω X Y α) (Q : X → Y → α → Prop) (ε : ℝ) : Prop

A public-coin finite-message protocol ε-satisfies a predicate Q if for every input (x, y), the probability that Q x y (p.rrun ...) fails is at most ε.

Equations

• p.ApproxSatisfies Q ε = ∀ (x : X) (y : Y), MeasureTheory.volume.real {ω : Ω | ¬Q x y (p.rrun x y ω)} ≤ ε

noncomputable def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.ApproxComputes {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} [MeasureTheory.MeasureSpace Ω] (p : Protocol Ω X Y α) (f : X → Y → α) (ε : ℝ) : Prop

A public-coin finite-message protocol ε-computes a function f if for every input (x, y), the probability of producing an incorrect answer is at most ε.

Equations

• p.ApproxComputes f ε = ∀ (x : X) (y : Y), MeasureTheory.volume.real {ω : Ω | p.rrun x y ω ≠ f x y} ≤ ε

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.ApproxComputes_eq_ApproxSatisfies {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} [MeasureTheory.MeasureSpace Ω] (p : Protocol Ω X Y α) (f : X → Y → α) (ε : ℝ) : p.ApproxComputes f ε = p.ApproxSatisfies (fun (x : X) (y : Y) (a : α) => a = f x y) ε

@[reducible, inline]

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

Convert a public-coin finite-message protocol to a binary public-coin protocol. Delegates to Deterministic.FiniteMessage.Protocol.toProtocol.

Equations

• p.toProtocol = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol p

@[simp]

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

@[simp]

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

@[reducible, inline]

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

Embed a binary public-coin protocol into a finite-message protocol. Delegates to Deterministic.FiniteMessage.Protocol.ofProtocol.

Equations

• CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.ofProtocol p = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol p

@[simp]

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

@[simp]

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

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.ofProtocol_equiv {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : PublicCoin.Protocol Ω X Y α) : ∃ (P : Protocol Ω X Y α), (∀ (x : X) (y : Y) (ω : Ω), P.rrun x y ω = p.rrun x y ω) ∧ Deterministic.FiniteMessage.Protocol.complexity P = Deterministic.Protocol.complexity p