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

The ε-error public-coin randomized communication complexity of f, defined as the minimum worst-case number of bits exchanged over all public-coin 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.PublicCoin.communicationComplexity_le_iff {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (ε : ℝ) (m : ℕ) : communicationComplexity f ε ≤ ↑m ↔ ∃ (n : ℕ) (p : Protocol (CoinTape n) X Y α), p.ApproxComputes f ε ∧ Deterministic.Protocol.complexity p ≤ m

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

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

theorem CommunicationComplexity.PublicCoin.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.PublicCoin.communicationComplexity_le_of_finiteMessage {X : Type u_2} {Y : Type u_3} {α : Type u_4} {Ω : Type u_1} [FiniteProbabilitySpace Ω] (f : X → Y → α) (ε ε' : ℝ) (hε : ε' < ε) (p : FiniteMessage.Protocol Ω X Y α) (hp : p.ApproxComputes f ε') : communicationComplexity f ε ≤ ↑(Deterministic.FiniteMessage.Protocol.complexity p)

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