Documentation

Complexity.Probability.Minimax

Averaging and the minimax principle for finite distributions #

Think of a two-player game in which one player picks a strategy a and the other an input b, with loss loss a b; for an algorithm, loss a b may be whether a errs on b. Drawing the strategy from a distribution μ and the input from a distribution ν relates the two classical guarantees of randomized algorithms [Yao77]. Distributions appear in two forms: finitely supported ones as points of the standard simplex (Convexity.StdSimplex), and probability mass functions (PMF), whose supports may be infinite. On a finite type the two correspond (Probability.PMF.ofStdSimplex, Probability.PMF.toStdSimplex).

Main definitions #

Main results #

References #

Finitely supported distributions #

source
theorem Convexity.StdSimplex.sum_mul_le_of_forall_le {α : Type u_1} {μ : StdSimplex ℝ α} {g : α → ℝ} {c : ℝ} (h : ∀ a ∈ μ.weights.support, g a ≤ c) :
(μ.weights.sum fun (a : α) (w : ℝ) => w * g a) ≤ c

An average under a finitely supported distribution is at most any bound on the support.

source
theorem Convexity.StdSimplex.exists_mem_support_le_sum_mul {α : Type u_1} (μ : StdSimplex ℝ α) (g : α → ℝ) :
∃ a ∈ μ.weights.support, g a ≤ μ.weights.sum fun (a : α) (w : ℝ) => w * g a

The averaging argument: some point of the support of a finitely supported distribution is at most the average.

The minimax theorem for finite games #

source
theorem Convexity.StdSimplex.exists_forall_sum_le_of_forall_exists_sum_le {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] (M : I → J → ℝ) {c : ℝ} (h : ∀ (q : StdSimplex ℝ J), ∃ (i : I), ∑ j : J, q.weights j * M i j ≤ c) :
∃ (p : StdSimplex ℝ I), ∀ (j : J), ∑ i : I, p.weights i * M i j ≤ c

The minimax theorem for finite two-player zero-sum games [Sio58], in the form used by Yao's principle. A row player picks i : I, a column player picks j : J, and the row player pays M i j. If against every mixed strategy q of the column player some row i has expected payment at most c, then some mixed strategy p of the row player has expected payment at most c against every column j.

Probability mass functions #

source
theorem Cslib.Probability.PMF.exists_mem_support_le_tsum_mul {α : Type u_1} (μ : PMF α) (g : α → ENNReal) :
∃ a ∈ μ.support, g a ≤ ∑' (a : α), μ a * g a

Some possible outcome is at most the mean: for every distribution μ and every function g with values in [0, ∞], some outcome a that μ can produce has g a at most the mean of g under μ. The sample space may be infinite.

source
theorem Cslib.Probability.PMF.exists_mem_support_tsum_mul_le {α : Type u_1} {β : Type u_2} (μ : PMF α) (ν : PMF β) (loss : α → β → ENNReal) {ε : ENNReal} (h : ∀ b ∈ ν.support, ∑' (a : α), μ a * loss a b ≤ ε) :
∃ a ∈ μ.support, ∑' (b : β), ν b * loss a b ≤ ε

The averaging argument, the easy direction of Yao's principle. Let loss a b be the loss of a strategy a on an input b. If drawing the strategy from μ has expected loss at most ε on every input that ν can produce, then some strategy that μ can produce has expected loss at most ε on inputs drawn from ν. The sample spaces may be infinite.

source
theorem Cslib.Probability.PMF.exists_mem_support_toOuterMeasure_le {α : Type u_1} {β : Type u_2} (μ : PMF α) (ν : PMF β) (E : α → β → Prop) {ε : ℝ} (h : ∀ b ∈ ν.support, (μ.toOuterMeasure {a : α | E a b}).toReal ≤ ε) :
∃ a ∈ μ.support, (ν.toOuterMeasure {b : β | E a b}).toReal ≤ ε

The averaging argument for events, the easy direction of Yao's principle: if a strategy drawn from μ fails on every input that ν can produce with probability at most ε, then some strategy that μ can produce fails on an input drawn from ν with probability at most ε. The sample spaces may be infinite.

The minimax theorem for probability mass functions #

source
def Cslib.Probability.PMF.ofStdSimplex {I : Type u_3} [Fintype I] (p : Convexity.StdSimplex ℝ I) :
PMF I

The distribution on a finite type whose probabilities are the weights of a point of the standard simplex.

Instances For
    source
    @[simp]
    theorem Cslib.Probability.PMF.toReal_ofStdSimplex {I : Type u_3} [Fintype I] (p : Convexity.StdSimplex ℝ I) (i : I) :
    ((ofStdSimplex p) i).toReal = p.weights i

    The probability of i under ofStdSimplex p is the weight of i in p.

    source
    noncomputable def Cslib.Probability.PMF.toStdSimplex {I : Type u_3} [Fintype I] (μ : PMF I) :
    Convexity.StdSimplex ℝ I

    The point of the standard simplex whose weights are the probabilities of a distribution on a finite type.

    Instances For
      source
      @[simp]
      theorem Cslib.Probability.PMF.weights_toStdSimplex {I : Type u_3} [Fintype I] (μ : PMF I) (i : I) :
      (toStdSimplex μ).weights i = (μ i).toReal

      The weight of i in toStdSimplex μ is the probability of i, as a real number.

      source
      @[simp]
      theorem Cslib.Probability.PMF.ofStdSimplex_toStdSimplex {I : Type u_3} [Fintype I] (μ : PMF I) :
      ofStdSimplex (toStdSimplex μ) = μ

      Passing from a distribution to the simplex and back returns the distribution.

      source
      theorem Cslib.Probability.PMF.exists_forall_sum_mul_le {I : Type u_3} {J : Type u_4} [Fintype I] [Fintype J] [Nonempty I] (M : I → J → ℝ) {ε : ℝ} (h : ∀ (ν : PMF J), ∃ (i : I), ∑ j : J, (ν j).toReal * M i j ≤ ε) :
      ∃ (μ : PMF I), ∀ (j : J), ∑ i : I, (μ i).toReal * M i j ≤ ε

      The minimax theorem for finite games [vN28], for distributions. Let M i j be the loss of a strategy i on an input j. If against every distribution ν on the inputs some strategy has expected loss at most ε, then some distribution μ on the strategies has expected loss at most ε on every input. This is the hard direction of Yao's principle; it is Convexity.StdSimplex.exists_forall_sum_le_of_forall_exists_sum_le, from Sion's theorem, read through ofStdSimplex.

      source
      theorem Cslib.Probability.PMF.exists_forall_toOuterMeasure_le {I : Type u_5} {J : Type u_6} [Finite J] [Nonempty I] (E : I → J → Prop) {ε : ℝ} (h : ∀ (ν : PMF J), ∃ (i : I), (ν.toOuterMeasure {j : J | E i j}).toReal ≤ ε) :
      ∃ (μ : PMF I), μ.support.Finite ∧ ∀ (j : J), (μ.toOuterMeasure {i : I | E i j}).toReal ≤ ε

      Yao's minimax principle for finite sets of inputs. Let E i j say that a strategy i fails on an input j, where there may be infinitely many strategies but only finitely many inputs. If against every distribution ν on the inputs some strategy fails with probability at most ε, then some distribution μ on finitely many strategies fails with probability at most ε on every input.