@[reducible, inline]

abbrev CommunicationComplexity.PublicCoin.OneWay.Protocol (Ω : Type u_1) (X : Type u_2) (Y : Type u_3) (α : Type u_4) : Type (max (max (max 1 u_2 u_1) u_3 u_1) u_4)

Equations

• CommunicationComplexity.PublicCoin.OneWay.Protocol Ω X Y α = CommunicationComplexity.Deterministic.OneWay.Protocol (Ω × X) (Ω × Y) α

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

Execute a one-way public-coin protocol on inputs x, y with shared randomness ω.

Equations

• p.rrun x y ω = p.decode (p.send (ω, x)) (ω, y)

noncomputable def CommunicationComplexity.PublicCoin.OneWay.Protocol.ApproxComputes {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} {α : Type u_4} [MeasureTheory.MeasureSpace Ω] (p : Protocol Ω X Y α) (f : X → Y → α) (ε : ℝ) : Prop

A one-way public-coin protocol ε-computes f if for every input pair (x, y), the error probability over shared randomness is at most ε.

Equations

• p.ApproxComputes f ε = ∀ (x : X) (y : Y), (MeasureTheory.volume {ω : Ω | p.rrun x y ω ≠ f x y}).toReal ≤ ε

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

The ε-error one-way public-coin communication complexity of f, defined as the minimum one-way message cost over all shared-randomness 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.OneWay.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.OneWay.Protocol.cost p ≤ m

theorem CommunicationComplexity.PublicCoin.OneWay.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.OneWay.Protocol.cost p

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