Public Coin Approximation

A public-coin finite-message protocol over an arbitrary finite probability space Ω can be approximated by one over CoinTape n.

noncomputable def CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toCoinTape {Ω : Type u_1} [FiniteProbabilitySpace Ω] {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (δ : ℝ) (hδ : 0 < δ) : (n : ℕ) × Protocol (CoinTape n) X Y α

Approximate a public-coin finite-message protocol over an arbitrary finite probability space by one over CoinTape. Given δ > 0, produces n and a CoinTape-based protocol with the same complexity.

Equations

• p.toCoinTape δ hδ = ⟨⋯.choose, CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap p (Prod.map ⋯.choose id) (Prod.map ⋯.choose id)⟩

@[simp]

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toCoinTape_complexity {Ω : Type u_1} [FiniteProbabilitySpace Ω] {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (δ : ℝ) (hδ : 0 < δ) : Deterministic.FiniteMessage.Protocol.complexity (p.toCoinTape δ hδ).snd = Deterministic.FiniteMessage.Protocol.complexity p

theorem CommunicationComplexity.PublicCoin.FiniteMessage.Protocol.toCoinTape_approxSatisfies {Ω : Type u_1} [FiniteProbabilitySpace Ω] {X : Type u_2} {Y : Type u_3} {α : Type u_4} (p : Protocol Ω X Y α) (Q : X → Y → α → Prop) (ε δ : ℝ) (hδ : 0 < δ) (hp : p.ApproxSatisfies Q ε) : (p.toCoinTape δ hδ).snd.ApproxSatisfies Q (ε + δ)

The CoinTape approximation of a public-coin protocol preserves ApproxSatisfies up to the given slack δ.