EconCSLib.GameTheory.ExtensiveGame.GameTreeNE

Nash equilibrium on GameTree, a weaker concept than subgame-perfect equilibrium.

An NE only requires optimality at the root (the entire game), allowing "incredible threats" off the equilibrium path. Every SPE is an NE, but not vice-versa — this is the classical distinction [MSZ §7.1].

Main definitions

• GameTree.IsNashEquilibrium — no unilateral deviation improves the root-game outcome.
• GameTree.IsNashAt — root-scoped alias for IsNashEquilibrium.
• GameTree.IsSubgamePerfectOn — root-scoped subgame-perfect predicate.
• GameTree.HasOnlyRootSubgames — every subgame of a fixed tree is the root.

Main results

• IsSubgamePerfect.toNE — SPE implies NE (as a corollary of Kuhn).
• IsSubgamePerfect.toSubgamePerfectOn — global SPE implies root-scoped SPE.
• isSubgamePerfectOn_iff_forall_subtree_isNashAt — subgame perfection on a root is exactly Nash equilibrium at every subtree.
• IsNashAt.toSubgamePerfectOn_of_hasOnlyRootSubgames — if a tree has no proper subgames, every root Nash equilibrium is subgame-perfect on that tree (MSZ Theorem 7.4, pure finite-tree form).

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

Nash equilibrium: no single player can improve their outcome at the root game by unilateral deviation.

Weaker than IsSubgamePerfect, which demands optimality at every subtree.

Equations

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

@[reducible, inline]

abbrev GameTree.IsNashAt {N : Type u_1} {U : Type u_2} [TotalPreorder U] (σ : Strategy N U) (g : GameTree N U) : Prop

Root-scoped Nash equilibrium predicate for a fixed GameTree root.

This is definitionally the existing IsNashEquilibrium, with the requested root-first API name for users who want to state equilibrium at a particular subgame rather than quantify over every subtree.

Equations

• GameTree.IsNashAt σ g = GameTree.IsNashEquilibrium σ g

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

Root-scoped subgame perfection on the subtrees of a fixed root.

IsSubgamePerfect σ is global over every GameTree N U. This predicate restricts the same no-profitable-deviation condition to subgames that occur inside the chosen root g.

Equations

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

def GameTree.HasOnlyRootSubgames {N : Type u_1} {U : Type u_2} (g : GameTree N U) : Prop

A fixed GameTree has no proper subgames when every subtree is the root itself. This is the pure finite-tree analogue of having no nontrivial subgames.

Equations

• g.HasOnlyRootSubgames = ∀ (s : GameTree N U), s.Subtree g → s = g

theorem GameTree.isSubgamePerfectOn_iff_forall_subtree_isNashAt {N : Type u_1} {U : Type u_2} [TotalPreorder U] {σ : Strategy N U} {g : GameTree N U} : IsSubgamePerfectOn σ g ↔ ∀ (s : GameTree N U), s.Subtree g → IsNashAt σ s

Root-scoped subgame perfection is equivalent to Nash equilibrium at every subtree of the root. This is the pure finite-tree form of MSZ Definition 7.2.

theorem GameTree.IsSubgamePerfect.toNE {N : Type u_1} {U : Type u_2} [TotalPreorder U] {σ : Strategy N U} (hspe : IsSubgamePerfect σ) (g : GameTree N U) : IsNashEquilibrium σ g

SPE ⇒ NE: every subgame-perfect equilibrium is a Nash equilibrium (at any fixed root game).

theorem GameTree.IsSubgamePerfect.toSubgamePerfectOn {N : Type u_1} {U : Type u_2} [TotalPreorder U] {σ : Strategy N U} (hspe : IsSubgamePerfect σ) (g : GameTree N U) : IsSubgamePerfectOn σ g

A global subgame-perfect equilibrium is subgame-perfect on every fixed root.

theorem GameTree.IsSubgamePerfectOn.toNashAt {N : Type u_1} {U : Type u_2} [TotalPreorder U] {σ : Strategy N U} {g : GameTree N U} (hspe : IsSubgamePerfectOn σ g) : IsNashAt σ g

Root-scoped subgame perfection implies Nash equilibrium at the same root.

theorem GameTree.IsNashAt.toSubgamePerfectOn_of_hasOnlyRootSubgames {N : Type u_1} {U : Type u_2} [TotalPreorder U] {σ : Strategy N U} {g : GameTree N U} (hnash : IsNashAt σ g) (hsubgames : g.HasOnlyRootSubgames) : IsSubgamePerfectOn σ g

If a tree has no proper subgames, root Nash equilibrium already implies subgame perfection on that tree. This is the pure finite-tree form of MSZ Theorem 7.4.

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

Kuhn's theorem, NE form: every finite perfect-information game without chance has a pure-strategy Nash equilibrium.

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

Kuhn's theorem, root-scoped SPE form: every finite perfect-information game without chance has a pure strategy that is subgame-perfect on that root.