noncomputable def CommunicationComplexity.PrivateCoin.communicationComplexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) : ℕ∞

The ε-error randomized communication complexity of f, defined as the minimum worst-case number of bits exchanged over all coin-flip randomized protocols that compute f with error at most ε on every input.

Equations

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

theorem CommunicationComplexity.PrivateCoin.communicationComplexity_le_iff {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (n : ℕ) : communicationComplexity f ε ≤ ↑n ↔ ∃ (nX : ℕ) (nY : ℕ) (p : Protocol (CoinTape nX) (CoinTape nY) X Y α), p.ApproxComputes f ε ∧ Deterministic.Protocol.complexity p ≤ n

theorem CommunicationComplexity.PrivateCoin.le_communicationComplexity_iff {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (n : ℕ) : ↑n ≤ communicationComplexity f ε ↔ ∀ (nX nY : ℕ) (p : Protocol (CoinTape nX) (CoinTape nY) X Y α), p.ApproxComputes f ε → n ≤ Deterministic.Protocol.complexity p

theorem CommunicationComplexity.PrivateCoin.communicationComplexity_le_iff_finiteMessage {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (n : ℕ) : communicationComplexity f ε ≤ ↑n ↔ ∃ (nX : ℕ) (nY : ℕ) (p : FiniteMessage.Protocol (CoinTape nX) (CoinTape nY) X Y α), p.ApproxComputes f ε ∧ Deterministic.FiniteMessage.Protocol.complexity p ≤ n

theorem CommunicationComplexity.PrivateCoin.communicationComplexity_mono {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) {ε ε' : ℝ} (h : ε' ≤ ε) : communicationComplexity f ε ≤ communicationComplexity f ε'

Communication complexity is monotone in ε: allowing more error can only make computation easier.

theorem CommunicationComplexity.PrivateCoin.communicationComplexity_le_of_finiteMessage {X : Type u_3} {Y : Type u_4} {α : Type u_5} {Ω_X : Type u_1} {Ω_Y : Type u_2} [FiniteProbabilitySpace Ω_X] [FiniteProbabilitySpace Ω_Y] (f : X → Y → α) (ε ε' : ℝ) (hε : ε' < ε) (p : FiniteMessage.Protocol Ω_X Ω_Y X Y α) (hp : p.ApproxComputes f ε') : communicationComplexity f ε ≤ ↑(Deterministic.FiniteMessage.Protocol.complexity p)

If a finite-message protocol over arbitrary finite probability spaces ε'-computes f with ε' < ε, then the private-coin communication complexity at error ε is at most the protocol's complexity.