EconCSLib.GameTheory.ExtensiveGame.GameTreeSPE

Strategies, outcomes, and Kuhn's theorem on GameTree N U: every finite perfect-information game without chance has a subgame-perfect equilibrium, obtainable via backward induction.

Minimal assumptions

Only [TotalPreorder U] — preorder + totality, no antisymmetry, no decidability. See ExtensiveGame/BackwardInduction.lean.

Main definitions

• GameTree.Strategy — a strategy is a subtype-bundled child-selector at every possible (mover, head, tail).
• GameTree.outcome — the terminal payoff reached when following a strategy.
• GameTree.optStrategy — the canonical backward-induction strategy (picks a child whose value attains the backward-induction max for the node's mover).
• GameTree.IVariant — two strategies differ only at nodes whose mover is i.
• GameTree.IsSubgamePerfect — no unilateral deviation of any player at any subgame improves their payoff.

Main results

• outcome_optStrategy_eq_value — outcome of optStrategy is the BI value.
• optStrategy_isSubgamePerfect — the backward-induction strategy optStrategy is a subgame-perfect equilibrium (the substantive theorem).
• Kuhn_exists_SPE — existence form: every finite perfect-information game has an SPE.

A note on the name "Kuhn"

"Kuhn's theorem" here means the backward-induction / SPE-existence theorem (Kuhn 1953). It is distinct from the other result also called Kuhn's theorem — the equivalence of mixed and behavioral strategies under perfect recall — whose infrastructure lives in ExtensiveGame/BehaviorStrategy.lean (tracked under EG-L2). Do not conflate the two.

References

• [MSZ, Ch. 3] Maschler, Solan, Zamir, Game Theory (Cambridge, 2013) — backward induction on finite perfect-information games.
• Kuhn, H. W. (1953), "Extensive Games and the Problem of Information," in Contributions to the Theory of Games, Vol. II.

Strategies

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

A pure strategy for the entire game tree: at every possible node context (mover, head, tail), specify one child (bundled with its membership proof).

Note: a single Strategy covers all players. Player-i "strategies" are conceptualized as the restriction to nodes where mover = i.

Equations

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

@[irreducible]

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

The outcome (terminal payoff vector) of playing strategy σ starting from game tree g. Walks down the tree, using σ to pick a child at each Node, until a Leaf is reached.

Equations

• GameTree.outcome σ (GameTree.Leaf p) = p
• GameTree.outcome σ (GameTree.Node m h t) = GameTree.outcome σ ↑(σ m h t)

@[simp]

theorem GameTree.outcome_Leaf {N : Type u_1} {U : Type u_2} (σ : Strategy N U) (p : N → U) : outcome σ (Leaf p) = p

@[simp]

theorem GameTree.outcome_Node {N : Type u_1} {U : Type u_2} (σ : Strategy N U) (m : N) (h : GameTree N U) (t : List (GameTree N U)) : outcome σ (Node m h t) = outcome σ ↑(σ m h t)

Backward-induction strategy

noncomputable def GameTree.optStrategy {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : Strategy N U

The canonical backward-induction strategy: at each node, pick a child whose backward-induction value equals the node's value (i.e., a child attaining the argmax for the mover).

Noncomputable — uses classical choice via value_Node_eq_some_child_value.

Equations

• GameTree.optStrategy m h t = ⟨⋯.choose, ⋯⟩

theorem GameTree.value_optStrategy_eq {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (m : N) (h : GameTree N U) (t : List (GameTree N U)) : (↑(optStrategy m h t)).value = (Node m h t).value

At a node, the optStrategy picks a child whose value equals the node's value.

Strategy deviation

def GameTree.IVariant {N : Type u_1} {U : Type u_2} (i : N) (σ σ' : Strategy N U) : Prop

Two strategies are i-variants if they agree on all nodes NOT owned by i. I.e., σ' is obtained from σ by changing only player i's choices.

Equations

• GameTree.IVariant i σ σ' = ∀ (m : N) (h : GameTree N U) (t : List (GameTree N U)), m ≠ i → σ m h t = σ' m h t

theorem GameTree.IVariant.refl {N : Type u_1} {U : Type u_2} (i : N) (σ : Strategy N U) : IVariant i σ σ

IVariant is reflexive: any strategy is an i-variant of itself.

Subgame-perfect equilibrium

def GameTree.IsSubgamePerfect {N : Type u_1} {U : Type u_2} [TotalPreorder U] (σ : Strategy N U) : Prop

A strategy is subgame-perfect (SPE) if, at every subtree, no player can strictly improve their payoff by a unilateral deviation — i.e., by switching to any i-variant strategy.

Equations

• GameTree.IsSubgamePerfect σ = ∀ (g : GameTree N U) (i : N) (σ' : GameTree.Strategy N U), GameTree.IVariant i σ σ' → GameTree.outcome σ' g i ≤ GameTree.outcome σ g i

Kuhn's theorem (main result)

theorem GameTree.outcome_optStrategy_eq_value {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (g : GameTree N U) : outcome optStrategy g = g.value

Key lemma: the outcome of the backward-induction strategy equals the backward-induction value vector at every game tree.

This is the bridge between value (defined via argmax) and outcome (defined via tree traversal).

theorem GameTree.optStrategy_isSubgamePerfect {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : IsSubgamePerfect optStrategy

Optimality of optStrategy: for every subtree g, every player i, and every i-variant deviation σ', the deviating outcome is no better than optStrategy's outcome at coordinate i. This is the SPE property spelled out before bundling into existence form.

theorem GameTree.Kuhn_exists_SPE {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : ∃ (σ : Strategy N U), IsSubgamePerfect σ

Kuhn's theorem (existence form): every finite perfect-information game without chance admits a subgame-perfect equilibrium.

The backward-induction strategy optStrategy is such an SPE.