EconCSLib.GameTheory.StrategicGame.Basic

Defines StrategicGame, the central structure of the library.

Main definitions

• StrategicGame — a strategic-form (normal-form) game
• StrategicGame.Profile — the type of strategy profiles for a game
• StrategicGame.deviate — unilateral deviation on a game-bound profile
• welfare — social welfare (sum of payoffs)

Design choices

• N (player type) and U (utility type) are unconstrained in the structure.
• strategy is a dependent family, so players may have different strategy spaces.
• Profile G = ∀ i, G.strategy i (a choice of strategy for each player).
• deviate σ i s' is owned by StrategicGame, not by a standalone core profile abstraction.

structure StrategicGame (N : Type u_1) (U : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

A strategic game (normal-form game) with players N and utilities in U.

The structure records only the bare data: strategy spaces and a payoff function. All assumptions (finiteness, ordering, computability) are added at usage sites.

• strategy : N → Type u_3

  The strategy space of each player.

• payoff : ((i : N) → self.strategy i) → N → U

  The payoff function: maps a strategy profile to each player's utility.

Profile

@[reducible, inline]

abbrev StrategicGame.Profile {N : Type u_1} {U : Type u_2} (G : StrategicGame N U) : Type (max u_1 u_3)

The type of strategy profiles for game G: each player picks a strategy.

This is a dependent function ∀ i, G.strategy i. The profile type is bound to the game, making it explicit that a profile belongs to a specific strategic game.

Equations

• G.Profile = ((i : N) → G.strategy i)

@[reducible, inline]

abbrev StrategicGame.deviate {N : Type u_1} {U : Type u_2} {G : StrategicGame N U} [DecidableEq N] (σ : G.Profile) (i : N) (s' : G.strategy i) : G.Profile

Unilateral deviation in a game-bound profile: player i switches to s', while all other players keep their current strategies.

Equations

• StrategicGame.deviate σ i s' = Function.update σ i s'

def StrategicGame.«term_[_↦_]» : Lean.TrailingParserDescr

σ[i ↦ s'] is the profile where player i switches to s'.

Scoped to keep the postfix […] bracket from clashing with list literals (… []) in importing files; open scoped StrategicGame to use it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem StrategicGame.Profile.deviate_self {N : Type u_1} {U : Type u_2} {G : StrategicGame N U} [DecidableEq N] (σ : G.Profile) (i : N) : deviate σ i (σ i) = σ

Deviating to the same strategy is the identity.

@[simp]

theorem StrategicGame.Profile.deviate_same {N : Type u_1} {U : Type u_2} {G : StrategicGame N U} [DecidableEq N] (σ : G.Profile) (i : N) (s' : G.strategy i) : deviate σ i s' i = s'

At the deviated player, the updated profile returns the new strategy.

@[simp]

theorem StrategicGame.Profile.deviate_of_ne {N : Type u_1} {U : Type u_2} {G : StrategicGame N U} [DecidableEq N] (σ : G.Profile) (i : N) (s' : G.strategy i) {j : N} (h : j ≠ i) : deviate σ i s' j = σ j

At every other player, the updated profile is unchanged.

Welfare

noncomputable def StrategicGame.welfare {N : Type u_1} {U : Type u_2} [Fintype N] [AddCommMonoid U] (G : StrategicGame N U) (σ : G.Profile) : U

The social welfare of a profile: the sum of all players' payoffs. Requires [Fintype N] and [AddCommMonoid U].

Equations

• G.welfare σ = ∑ i : N, G.payoff σ i