noncomputable def CommunicationComplexity.Deterministic.OneWay.Protocol.distributionalError {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (μ : FiniteProbabilitySpace (X × Y)) (f : X → Y → α) : ℝ

The distributional error of a deterministic one-way protocol with respect to a distribution μ on X × Y: the probability that the protocol output disagrees with f.

Equations

• p.distributionalError μ f = (MeasureTheory.volume {xy : X × Y | p.run xy.1 xy.2 ≠ f xy.1 xy.2}).toReal

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

Fix the public randomness ω in a one-way public-coin protocol, producing a deterministic one-way protocol.

Equations

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

@[simp]

theorem CommunicationComplexity.PublicCoin.OneWay.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.OneWay.Protocol.toDeterministic_cost {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (ω : Ω) : (p.toDeterministic ω).cost = Deterministic.OneWay.Protocol.cost p

theorem CommunicationComplexity.PublicCoin.OneWay.minimax_lower_bound {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (n : ℕ) (μ : FiniteProbabilitySpace (X × Y)) (h : ∀ (p : Deterministic.OneWay.Protocol X Y α), p.cost ≤ n → p.distributionalError μ f > ε) : ↑n < communicationComplexity f ε

Yao's minimax principle (one direction) for one-way public-coin protocols: if some joint distribution μ forces every deterministic one-way protocol of cost at most n to have distributional error strictly greater than ε, then one-way public-coin communication complexity at error ε is greater than n.