noncomputable def CommunicationComplexity.Deterministic.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 protocol with respect to a distribution μ on X × Y: the probability that the protocol output disagrees with f.

Equations

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

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

Yao's minimax principle (one direction): if there exists a joint distribution μ over X × Y such that every deterministic protocol of complexity ≤ n fails with probability > ε under μ, then the public-coin randomized communication complexity of f at error ε is greater than n.