Define expected payoffs for mixed strategies¶

This page shows how to represent mixed strategies in Lean and define the expected payoff of a pair of them, for any symmetric game with finitely many actions. The definitions of the tutorial then apply to mixed strategies without change.

Mixed strategies from Mathlib¶

A mixed strategy over a finite set of actions assigns each action a probability. Mathlib already has the set of such assignments, the standard simplex stdSimplex ℝ Action: the functions from actions to real numbers that are non-negative and sum to one. It needs import Mathlib.Analysis.Convex.StdSimplex, and the type of actions must be finite.

A member of the simplex can be applied to an action like a function, so for a mixed strategy mine, mine first is the probability it gives the action first. Mathlib also provides stdSimplex.zero_le and stdSimplex.sum_eq_one, the two facts that make it a probability distribution.

The expected payoff¶

When the player uses mine and the opponent theirs, the pair of actions \((a, b)\) is played with probability \(x_a y_b\), and the expected payoff is the weighted sum

\[ u(x, y) = \sum_{a} \sum_{b} x_a \, y_b \, \pi(a, b), \]

where \(\pi\) is the payoff between pure actions. In Lean:

/-- The expected payoff to a player using the mixed strategy `mine` against an
opponent using `theirs`: each pair of actions contributes its payoff, weighted
by the probability that the pair is played. -/
def expectedPayoff {Action : Type} [Fintype Action] (payoff : Action → Action → ℝ)
    (mine theirs : stdSimplex ℝ Action) : ℝ :=
  ∑ first, ∑ second, mine first * theirs second * payoff first second

[Fintype Action] asks Lean to confirm that the actions are finite, which is what makes the sums meaningful.

Pure strategies¶

A pure strategy is the mixed strategy that puts probability one on a single action, which Mathlib calls stdSimplex.vertex. It needs to decide whether two actions are equal, hence [DecidableEq Action]. A good first check on the definition is that it recovers the payoff matrix on pure strategies:

theorem expectedPayoff_vertex {Action : Type} [Fintype Action] [DecidableEq Action]
    (payoff : Action → Action → ℝ) (first second : Action) :
    expectedPayoff payoff (stdSimplex.vertex first) (stdSimplex.vertex second) =
      payoff first second := by
  simp [expectedPayoff, Pi.single_apply]

The tutorial's definitions, for free¶

IsSymmetricNash and IsESS take any type of strategies and any payoff function on it. The simplex is a type and expectedPayoff payoff is a payoff function on it, so both definitions, and the capstone theorem, apply to mixed strategies directly:

/-- The capstone applies to mixed strategies without change. -/
example {Action : Type} [Fintype Action] {payoff : Action → Action → ℝ}
    {resident : stdSimplex ℝ Action} (stable : IsESS (expectedPayoff payoff) resident) :
    IsSymmetricNash (expectedPayoff payoff) resident :=
  stable.isSymmetricNash

This is the design decision of the tutorial paying off: because the capstone never looked inside the payoff function, it holds for mixed strategies with no further work.

The file needs import GameTheory.Capstone for this to work. Without it the error does not mention imports:

error: GameTheory/HowTo/MixedPayoff.lean:22:9: Invalid field `isSymmetricNash`: The environment does not contain `Function.isSymmetricNash`, so it is not possible to project the field `isSymmetricNash` from an expression

Lean could not find IsESS.isSymmetricNash, unfolded IsESS to the ∀ statement underneath, and looked for the theorem there instead.

A finite type of actions¶

For a game of our own, Lean must be told that its actions are finite. The usual way is deriving Fintype, but at the Mathlib version these notes use it fails on a plain type of actions, with an internal error reporting that the rewrite tactic failed. Writing the instance by hand avoids the problem:

/-- There are exactly two postures. -/
instance : Fintype Posture where
  elems := {hawk, dove}
  complete := by
    intro posture
    cases posture <;> simp

elems lists the actions, and complete proves that the list is complete. For proofs about a specific game it also helps to have a lemma that expands a sum over its actions:

/-- A sum over postures has two terms. -/
theorem sum_posture (f : Posture → ℝ) : ∑ posture, f posture = f hawk + f dove :=
  Fintype.sum_eq_add hawk dove (by decide) (by
    intro posture both
    cases posture <;> simp at both)

Verify a mixed ESS in Hawk-Dove uses all of this on a complete example.