@[reducible, inline]

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

A public-coin protocol is a deterministic protocol where both Alice and Bob see shared randomness Ω. Alice's input is (ω, x) and Bob's is (ω, y).

Equations

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

def CommunicationComplexity.PublicCoin.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 protocol.

Equations

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

def CommunicationComplexity.PublicCoin.Protocol.alice {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (f : X → Ω → Bool) (P : Bool → Protocol Ω X Y α) : Protocol Ω X Y α

Alice sends a bit depending on her input x and shared randomness ω.

Equations

• CommunicationComplexity.PublicCoin.Protocol.alice f P = CommunicationComplexity.Deterministic.Protocol.alice (fun (x : Ω × X) => match x with | (ω, x) => f x ω) P

def CommunicationComplexity.PublicCoin.Protocol.bob {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (f : Y → Ω → Bool) (P : Bool → Protocol Ω X Y α) : Protocol Ω X Y α

Bob sends a bit depending on his input y and shared randomness ω.

Equations

• CommunicationComplexity.PublicCoin.Protocol.bob f P = CommunicationComplexity.Deterministic.Protocol.bob (fun (x : Ω × Y) => match x with | (ω, y) => f y ω) P

def CommunicationComplexity.PublicCoin.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 protocol on inputs x, y with shared randomness ω.

Equations

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

@[simp]

theorem CommunicationComplexity.PublicCoin.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.Protocol.run p (ω, x) (ω, y)

def CommunicationComplexity.PublicCoin.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 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 {ω : Ω | ¬Q x y (p.rrun x y ω)}).toReal ≤ ε

noncomputable def CommunicationComplexity.PublicCoin.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 protocol ε-computes a function f if for every input (x, y), the probability (under the shared coin-flip measure) of producing an incorrect answer is at most ε.

Equations

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

theorem CommunicationComplexity.PublicCoin.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) ε