EconCSLib.GameTheory.ExtensiveGame.GameTreeStrategicForm

Strategic-form extraction for finite perfect-information GameTree games.

The extracted normal-form game gives every player a complete contingent plan: at each node context (mover, head, tail), choose one of the available children. During play, the node's mover selects which player's plan is used.

Main definitions

• GameTree.PlayerStrategy — one player's contingent plan on a GameTree.
• GameTree.profileStrategy — combine a normal-form profile into a global tree strategy.
• GameTree.toStrategicGame — extracted pure normal-form game.

Main results

• toStrategicGame_nash_iff_isNashAt — pure Nash in the extracted game is exactly root-scoped Nash in the original tree.

def GameTree.PlayerStrategy (N : Type u_3) (U : Type u_4) : Type (max u_3 u_4)

A single player's pure strategy in the normal form of a GameTree: a complete contingent plan choosing a child at every possible node.

Equations

• GameTree.PlayerStrategy N U = (N → (h : GameTree N U) → (t : List (GameTree N U)) → { c : GameTree N U // c ∈ h :: t })

def GameTree.profileStrategy {N : Type u_1} {U : Type u_2} (σ : N → PlayerStrategy N U) : Strategy N U

Combine a normal-form profile into the global GameTree.Strategy used by the game-tree evaluator. At each node, the mover's contingent plan is used.

Equations

• GameTree.profileStrategy σ m h t = σ m m h t

noncomputable def GameTree.toStrategicGame {N : Type u_1} {U : Type u_2} (g : GameTree N U) : StrategicGame N U

The strategic-form extraction of a finite perfect-information tree.

Equations

• g.toStrategicGame = { strategy := fun (x : N) => GameTree.PlayerStrategy N U, payoff := fun (σ : N → GameTree.PlayerStrategy N U) (i : N) => GameTree.outcome (GameTree.profileStrategy σ) g i }

theorem GameTree.profileStrategy_deviate_variant {N : Type u_1} {U : Type u_2} [DecidableEq N] (σ : N → PlayerStrategy N U) (i : N) (s' : PlayerStrategy N U) : IVariant i (profileStrategy σ) (profileStrategy (Function.update σ i s'))

Replacing player i's normal-form contingent plan produces an i-variant global tree strategy.

theorem GameTree.profileStrategy_deviate_eq_of_variant {N : Type u_1} {U : Type u_2} [DecidableEq N] (σ : N → PlayerStrategy N U) (i : N) (τ : Strategy N U) (hτ : IVariant i (profileStrategy σ) τ) : profileStrategy (Function.update σ i τ) = τ

Any global i-variant tree strategy can be represented by deviating player i's normal-form contingent plan.

theorem GameTree.toStrategicGame_nash_iff_isNashAt {N : Type u_1} {U : Type u_2} [DecidableEq N] [TotalPreorder U] (g : GameTree N U) (σ : g.toStrategicGame.Profile) : _root_.IsNashEquilibrium g.toStrategicGame σ ↔ IsNashAt (profileStrategy σ) g

Nash equilibrium in the extracted strategic-form game is exactly Nash equilibrium at the root of the original tree.