pure_nash_of_common_payoff_maximizer

theoremverified

In a strategic-form game G where all players have the same payoff function u (that is, G.payoff i s = u s for every player i and strategy profile s), any strategy profile s that globally maximizes u (that is, u s' ≤ u s for all strategy profiles s') is a pure Nash equilibrium.

Statement

theorem pure_nash_of_common_payoff_maximizer {Player : Type*} [DecidableEq Player]
    (G : StrategicGame Player) (u : (∀ j, G.Strategy j) → ℝ)
    (h_common : ∀ (i : Player) (s : ∀ j, G.Strategy j), G.payoff i s = u s)
    (s : ∀ i, G.Strategy i)
    (h_max : ∀ s' : ∀ j, G.Strategy j, u s' ≤ u s) :
    is_pure_nash_equilibrium G s

Source

Monderer & Shapley 1996, Potential Games, Theorem 2.1; Osborne & Rubinstein, A Course in Game Theory, Example 16.1

Verified

07 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 2

StrategicGameA strategic-form game with player type Player consists of a family of strategy types Strategy i for each player i : Player, and a…
is_pure_nash_equilibriumIn a strategic-form game G with player type Player, a strategy profile s : ∀ i, G.Strategy i is a pure Nash equilibrium if for every…

Read back from the Lean

Let Player be a type with decidable equality, and let G be a strategic game on Player. Suppose there exists a function u : (∀ j, G.Strategy j) → ℝ such that for every player i and every strategy profile s', player i's payoff G.payoff i s' equals u s'. If s is a strategy profile such that u s' ≤ u s for all strategy profiles s', then s is a pure Nash equilibrium of G.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- In a common-payoff game, any strategy profile that globally maximizes the common payoff is a pure Nash equilibrium. -/
theorem pure_nash_of_common_payoff_maximizer {Player : Type*} [DecidableEq Player]
    (G : StrategicGame Player) (u : (∀ j, G.Strategy j) → ℝ)
    (h_common : ∀ (i : Player) (s : ∀ j, G.Strategy j), G.payoff i s = u s)
    (s : ∀ i, G.Strategy i)
    (h_max : ∀ s' : ∀ j, G.Strategy j, u s' ≤ u s) :
    is_pure_nash_equilibrium G s := by
  intro i s_i'
  rw [h_common, h_common]
  exact h_max (Function.update s i s_i')

Discuss this result Challenge it