@[reducible, inline]

abbrev CommunicationComplexity.PrivateCoin.Protocol (Ω_X : Type u_1) (Ω_Y : Type u_2) (X : Type u_3) (Y : Type u_4) (α : Type u_5) : Type (max (max (max u_3 u_1) u_4 u_2) u_5)

A private-coin protocol is a deterministic protocol where Alice's input is augmented with private randomness Ω_X and Bob's with Ω_Y. Alice's message function sees (ω_x, x) and Bob's sees (ω_y, y).

Equations

• CommunicationComplexity.PrivateCoin.Protocol Ω_X Ω_Y X Y α = CommunicationComplexity.Deterministic.Protocol (Ω_X × X) (Ω_Y × Y) α

def CommunicationComplexity.PrivateCoin.Protocol.output {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_3} {Y : Type u_4} {α : Type u_5} (a : α) : Protocol Ω_X Ω_Y X Y α

Output node for a private-coin protocol.

Equations

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

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

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

Equations

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

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

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

Equations

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

def CommunicationComplexity.PrivateCoin.Protocol.rrun {Ω_X : Type u_1} {Ω_Y : Type u_2} {X : Type u_3} {Y : Type u_4} {α : Type u_5} (p : Protocol Ω_X Ω_Y X Y α) (x : X) (y : Y) (ω_x : Ω_X) (ω_y : Ω_Y) : α

Execute a private-coin protocol on inputs x, y with private randomness ω_x for Alice and ω_y for Bob.

Equations

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

@[simp]

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

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

A private-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 {ω : Ω_X × Ω_Y | ¬Q x y (p.rrun x y ω.1 ω.2)}).toReal ≤ ε

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

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

Equations

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

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