Documentation

Complexity.Computability.Communication.Distributional

Distributional complexity and Yao's minimax principle #

The distributional complexity D^ν_ε(R) of a relation R under a distribution ν on the pairs of inputs is the least depth of a deterministic protocol that errs with probability at most ε on inputs drawn from ν (Protocol.distributionalComplexity) Kushilevitz and Nisan, Chapter 3.

Yao's minimax principle [Yao77] says that randomized protocols are exactly as good as deterministic protocols against the hardest distribution: the public-coin complexity of R on A × B with error ε is the largest distributional complexity with error ε under a distribution on A × B (PublicCoin.ecomplexity_eq_iSup_distributionalComplexity), when the inputs are finite and there is some output. One direction is the averaging argument (PublicCoin.distributionalComplexity_le_ecomplexity): a public-coin protocol erring with probability at most ε on every input draws, for every ν, some deterministic protocol erring with probability at most ε on inputs drawn from ν. The other follows from von Neumann's minimax theorem for the game in which one player picks a deterministic protocol sending at most c bits and the other a pair of inputs (PublicCoin.ecomplexity_le_of_forall_distributionalComplexity_le, from Probability.PMF.exists_forall_toOuterMeasure_le). So lower bounds on randomized protocols are exactly lower bounds on deterministic protocols over a well-chosen distribution.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Communication.Protocol.distributionalComplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (ε : ℝ) (R : X → Y → Z → Prop) (ν : PMF (X × Y)) :
ℕ∞

The distributional complexity D^ν_ε(R) of R under a distribution ν on the pairs of inputs: the least depth of a deterministic protocol whose output on a pair of inputs drawn from ν is not related to them by R with probability at most ε, or ⊤ if there is none.

Instances For
    source
    theorem Cslib.Communication.Protocol.distributionalComplexity_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {ε : ℝ} {R : X → Y → Z → Prop} {ν : PMF (X × Y)} (hp : p.distributionalError ν R ≤ ε) :
    distributionalComplexity ε R ν ≤ ↑p.depth
    source
    theorem Cslib.Communication.Protocol.le_distributionalComplexity_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {ν : PMF (X × Y)} {k : ℕ∞} :
    k ≤ distributionalComplexity ε R ν ↔ ∀ (p : Protocol X Y Z), p.distributionalError ν R ≤ ε → k ≤ ↑p.depth
    source
    theorem Cslib.Communication.Protocol.distributionalComplexity_le_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {ν : PMF (X × Y)} {k : ℕ} :
    distributionalComplexity ε R ν ≤ ↑k ↔ ∃ (p : Protocol X Y Z), p.distributionalError ν R ≤ ε ∧ p.depth ≤ k
    source
    theorem Cslib.Communication.Protocol.distributionalComplexity_anti {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε ε' : ℝ} {R : X → Y → Z → Prop} {ν : PMF (X × Y)} (hε : ε ≤ ε') :
    distributionalComplexity ε' R ν ≤ distributionalComplexity ε R ν

    Allowing more error makes a relation easier.

    source
    theorem Cslib.Communication.PublicCoin.distributionalComplexity_le_ecomplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ν : PMF (X × Y)} (hν : ∀ q ∈ ν.support, q.1 ∈ A ∧ q.2 ∈ B) :
    Protocol.distributionalComplexity ε R ν ≤ ecomplexity ε R A B

    Yao's principle, the easy direction: under every distribution ν on A × B, the distributional complexity with error ε is at most the public-coin complexity on A × B with error ε.

    source
    theorem Cslib.Communication.PublicCoin.ecomplexity_le_of_forall_distributionalComplexity_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} [Finite X] [Finite Y] [Nonempty Z] {c : ℕ} (h : ∀ (ν : PMF (X × Y)), (∀ q ∈ ν.support, q.1 ∈ A ∧ q.2 ∈ B) → Protocol.distributionalComplexity ε R ν ≤ ↑c) :
    ecomplexity ε R A B ≤ ↑c

    Yao's principle, the hard direction: on finite inputs, if under every distribution on A × B some deterministic protocol sending at most c bits errs with probability at most ε, then some public-coin protocol sending at most c bits errs with probability at most ε on every pair of inputs from A × B. The protocol draws from finitely many deterministic protocols.

    source
    theorem Cslib.Communication.PublicCoin.ecomplexity_le_iff_forall_distributionalComplexity_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} [Finite X] [Finite Y] [Nonempty Z] {c : ℕ} :
    ecomplexity ε R A B ≤ ↑c ↔ ∀ (ν : PMF (X × Y)), (∀ q ∈ ν.support, q.1 ∈ A ∧ q.2 ∈ B) → Protocol.distributionalComplexity ε R ν ≤ ↑c

    Yao's principle: on finite inputs, the public-coin complexity on A × B with error ε is at most c exactly when the distributional complexity with error ε is at most c under every distribution on A × B.

    source
    theorem Cslib.Communication.PublicCoin.ecomplexity_eq_iSup_distributionalComplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} [Finite X] [Finite Y] [Nonempty Z] :
    ecomplexity ε R A B = ⨆ (ν : PMF (X × Y)), ⨆ (_ : ∀ q ∈ ν.support, q.1 ∈ A ∧ q.2 ∈ B), Protocol.distributionalComplexity ε R ν

    Yao's minimax principle Kushilevitz and Nisan, Theorem 3.20: on finite inputs, the public-coin complexity on A × B with error ε is the largest distributional complexity with error ε under a distribution on A × B.

    source
    theorem Cslib.Communication.PublicCoin.ecomplexityFun_eq_iSup_distributionalComplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} [Finite X] [Finite Y] [Nonempty Z] (f : X → Y → Z) :
    ecomplexityFun ε f = ⨆ (ν : PMF (X × Y)), Protocol.distributionalComplexity ε (fun (x : X) (y : Y) (z : Z) => f x y = z) ν

    Yao's minimax principle for computing a function: on finite inputs, the public-coin complexity of f with error ε is the largest distributional complexity of f with error ε.