EconCSLib.GameTheory.ExtensiveGame.ZeroSumGameTreeWithChance

2-player zero-sum extensive game with rational chance (Nature) nodes.

This module sits strictly between the chance-free Zermelo.lean and the fully general StochasticGameTree.lean (which requires vNM utility theory). Because payoffs and probabilities are both in ℚ, rational arithmetic suffices for chance averaging — no vNM theorem is needed.

Ported from math-xmum/gametheory (finitegame branch), GameTheory/ZerosumFiniteGame.lean, with EconCSLib-style docstrings and targeted imports (no import Mathlib).

Design

inductive GameTree
  | Leaf  (val : ℚ)                          -- terminal payoff for player A
  | Pnode (p : Player) (L R : GameTree)       -- player decision node (binary)
  | Nnode (p : Set.Icc (0:ℚ) 1) (L R : GameTree)  -- chance node (prob p → L)

value : GameTree → ℚ computes the backward-induction value for player A:

• Leaf → the leaf payoff.
• Player A node → max of children's values.
• Player B node → min of children's values.
• Nature node → probability-weighted average of children's values.

DStrategy : Strategy is A's canonical optimal (dominant) strategy: always choose the child with the higher value.

value_prop is the soundness theorem: for every B-strategy SB, t.value ≤ t.outcome DStrategy SB.

Main definitions

• ZeroSumChance.Player — two players: A (maximizer) and B (minimizer).
• ZeroSumChance.Select — binary selection: l (left) or r (right).
• ZeroSumChance.GameTree — inductive binary game tree with Nature.
• ZeroSumChance.GameTree.value — backward-induction value (computable).
• ZeroSumChance.GameTree.DStrategy — dominant strategy for A.
• ZeroSumChance.GameTree.outcome — outcome under a strategy pair.
• ZeroSumChance.GameTree.value_prop — t.value ≤ t.outcome DStrategy SB.

References

• Ported from math-xmum/gametheory finitegame branch, ZerosumFiniteGame.lean.
• [MSZ] Maschler, Solan, Zamir, Game Theory, §3.6 (Zermelo / finite games).

Related modules

• EconCSLib.GameTheory.ExtensiveGame.Zermelo — the chance-free variant.
• EconCSLib.GameTheory.ExtensiveGame.StochasticGameTree — n-player general utility (needs vNM).

Players and binary selection

inductive ZeroSumChance.Player : Type

The two players in a zero-sum game: A is the maximizer, B is the minimizer.

• A : Player
• B : Player

@[implicit_reducible]

instance ZeroSumChance.instReprPlayer : Repr Player

Equations

• ZeroSumChance.instReprPlayer = { reprPrec := ZeroSumChance.instReprPlayer.repr }

def ZeroSumChance.instReprPlayer.repr : Player → ℕ → Std.Format

Equations

• ZeroSumChance.instReprPlayer.repr ZeroSumChance.Player.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ZeroSumChance.Player.A")).group prec✝
• ZeroSumChance.instReprPlayer.repr ZeroSumChance.Player.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ZeroSumChance.Player.B")).group prec✝

@[implicit_reducible]

instance ZeroSumChance.instDecidableEqPlayer : DecidableEq Player

Equations

• ZeroSumChance.instDecidableEqPlayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ZeroSumChance.Select : Type

A binary choice: l = left branch, r = right branch.

• l : Select
• r : Select

@[implicit_reducible]

instance ZeroSumChance.instReprSelect : Repr Select

Equations

• ZeroSumChance.instReprSelect = { reprPrec := ZeroSumChance.instReprSelect.repr }

def ZeroSumChance.instReprSelect.repr : Select → ℕ → Std.Format

Equations

• ZeroSumChance.instReprSelect.repr ZeroSumChance.Select.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ZeroSumChance.Select.l")).group prec✝
• ZeroSumChance.instReprSelect.repr ZeroSumChance.Select.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ZeroSumChance.Select.r")).group prec✝

@[implicit_reducible]

instance ZeroSumChance.instDecidableEqSelect : DecidableEq Select

Equations

• ZeroSumChance.instDecidableEqSelect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Game tree

inductive ZeroSumChance.GameTree : Type

A finite binary game tree for a 2-player zero-sum game with Nature.

• Leaf val — terminal node; val is A's payoff (B gets -val).
• Pnode p L R — player p's decision node; player chooses L or R.
• Nnode prob L R — Nature's chance node; Nature picks L with probability prob ∈ [0,1] and R with probability 1 - prob.

• Leaf (val : ℚ) : GameTree
• Pnode (p : Player) (L R : GameTree) : GameTree
• Nnode (prob : ↑(Set.Icc 0 1)) (L R : GameTree) : GameTree

def ZeroSumChance.instReprGameTree.repr : GameTree → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZeroSumChance.instReprGameTree : Repr GameTree

Equations

• ZeroSumChance.instReprGameTree = { reprPrec := ZeroSumChance.instReprGameTree.repr }

def ZeroSumChance.instDecidableEqGameTree.decEq (x✝ x✝¹ : GameTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ZeroSumChance.instDecidableEqGameTree.decEq ([L a]) ([L b]) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq ([L val]) (ZeroSumChance.GameTree.Pnode p L R) = isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq ([L val]) (ZeroSumChance.GameTree.Nnode prob L R) = isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq (ZeroSumChance.GameTree.Pnode p L R) ([L val]) = isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq (ZeroSumChance.GameTree.Pnode p L R) (ZeroSumChance.GameTree.Nnode prob L_1 R_1) = isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq (ZeroSumChance.GameTree.Nnode prob L R) ([L val]) = isFalse ⋯
• ZeroSumChance.instDecidableEqGameTree.decEq (ZeroSumChance.GameTree.Nnode prob L R) (ZeroSumChance.GameTree.Pnode p L_1 R_1) = isFalse ⋯

@[implicit_reducible]

instance ZeroSumChance.instDecidableEqGameTree : DecidableEq GameTree

Equations

• ZeroSumChance.instDecidableEqGameTree = ZeroSumChance.instDecidableEqGameTree.decEq

@[implicit_reducible]

instance ZeroSumChance.instInhabitedGameTree : Inhabited GameTree

Equations

• ZeroSumChance.instInhabitedGameTree = { default := [L 0] }

Structural size

def ZeroSumChance.GameTree.size : GameTree → ℕ

Structural size of a game tree (used internally for well-founded reasoning).

Equations

• [L a].size = 1
• (ZeroSumChance.GameTree.Pnode a a_1 a_2).size = a_1.size + a_2.size
• (ZeroSumChance.GameTree.Nnode a a_1 a_2).size = a_1.size + a_2.size

theorem ZeroSumChance.GameTree.size_pos (t : GameTree) : 1 ≤ t.size

Every game tree has positive size.

Strategies and value

@[reducible, inline]

abbrev ZeroSumChance.GameTree.Strategy : Type

A pure strategy is a function that, given a player's decision node, selects one of the two branches. Strategy ≝ GameTree → GameTree → Select.

Equations

• ZeroSumChance.GameTree.Strategy = (ZeroSumChance.GameTree → ZeroSumChance.GameTree → ZeroSumChance.Select)

def ZeroSumChance.GameTree.value : GameTree → ℚ

The backward-induction value of the game tree for player A.

• A-node: A maximizes, so we take the max of both children's values.
• B-node: B minimizes, so we take the min of both children's values.
• Nature node: probability-weighted average (rational arithmetic).

Equations

• [L a].value = a
• (ZeroSumChance.GameTree.Pnode ZeroSumChance.Player.A a_1 a_2).value = max a_1.value a_2.value
• (ZeroSumChance.GameTree.Pnode ZeroSumChance.Player.B a_1 a_2).value = min a_1.value a_2.value
• (ZeroSumChance.GameTree.Nnode a a_1 a_2).value = ↑a * a_1.value + (1 - ↑a) * a_2.value

def ZeroSumChance.GameTree.DStrategy : Strategy

A's dominant strategy: at each A-node, move to whichever child has the higher value; ties go left.

Equations

• L.DStrategy R = if L.value < R.value then ZeroSumChance.Select.r else ZeroSumChance.Select.l

Outcome under a strategy pair

def ZeroSumChance.GameTree.outcome (SA SB : Strategy) : GameTree → ℚ

The realized payoff for player A when A plays SA and B plays SB.

Nature's moves are resolved by their fixed probabilities.

Equations

• One or more equations did not get rendered due to their size.
• ZeroSumChance.GameTree.outcome SA SB ([L a]) = a
• ZeroSumChance.GameTree.outcome SA SB (ZeroSumChance.GameTree.Nnode a a_1 a_2) = ↑a * ZeroSumChance.GameTree.outcome SA SB a_1 + (1 - ↑a) * ZeroSumChance.GameTree.outcome SA SB a_2

Main theorem

theorem ZeroSumChance.GameTree.value_prop (SB : Strategy) {t : GameTree} : t.value ≤ outcome DStrategy SB t

Soundness of DStrategy: the backward-induction value is a lower bound on the outcome A achieves by following DStrategy, regardless of how B plays.

Formally: for every B-strategy SB and game tree t, t.value ≤ t.outcome DStrategy SB.

Notation helpers

def ZeroSumChance.PUInterval (a : ℚ) : ↑(Set.Icc 0 1)

Coerce a rational a to the unit-interval subtype, defaulting to ⟨0, …⟩ if a ∉ [0, 1].

Equations

• ZeroSumChance.PUInterval a = if h : 0 ≤ a ∧ a ≤ 1 then ⟨a, h⟩ else ⟨0, ZeroSumChance.PUInterval._proof_1⟩

def ZeroSumChance.«term[L_]» : Lean.ParserDescr

Equations

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

def ZeroSumChance.«term[N_,_,_]» : Lean.ParserDescr

Equations

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

def ZeroSumChance.«term[A_,_]» : Lean.ParserDescr

Equations

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

def ZeroSumChance.«term[B_,_]» : Lean.ParserDescr

Equations

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

Quick smoke test