@[reducible, inline]

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

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

Equations

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

def CommunicationComplexity.PrivateCoin.FiniteMessage.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 finite-message protocol.

Equations

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

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

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

Equations

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

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

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

Equations

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

def CommunicationComplexity.PrivateCoin.FiniteMessage.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 finite-message protocol on inputs x, y with private randomness ω_x for Alice and ω_y for Bob.

Equations

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

@[simp]

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

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

noncomputable def CommunicationComplexity.PrivateCoin.FiniteMessage.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 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 {ω : Ω_X × Ω_Y | p.rrun x y ω.1 ω.2 ≠ f x y} ≤ ε

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

@[reducible, inline]

noncomputable abbrev CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toProtocol {Ω_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 α) : PrivateCoin.Protocol Ω_X Ω_Y X Y α

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

Equations

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

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toProtocol_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) : p.toProtocol.rrun x y ω_x ω_y = p.rrun x y ω_x ω_y

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toProtocol_complexity {Ω_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 α) : Deterministic.Protocol.complexity p.toProtocol = Deterministic.FiniteMessage.Protocol.complexity p

@[reducible, inline]

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

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

Equations

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

@[simp]

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

@[simp]

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

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