EconCSLib.GameTheory.ExtensiveGame.BackwardInduction

Backward induction on GameTree N U, producing a value function value : GameTree N U → (N → U) together with the optimality lemmas used by ExtensiveGame.SPE to prove Kuhn's theorem.

Minimal assumptions

The payoff type U carries [TotalPreorder U] (reflexivity + transitivity + totality; no antisymmetry) plus [DecidableLE U] so the argmax — and hence value — is computable. ℚ (the Zermelo / examples track) supplies both.

Main definitions

• GameTree.value — the backward-induction value vector (computable).
• GameTree.valueList — mutually recursive helper: value on a list of trees.

Main results

• value_Leaf — value of a leaf is its payoff
• value_Node — value of a node equals the argmax-chosen child's value
• value_Node_ge — the mover's coordinate dominates every child's
• value_Node_eq_some_child_value — a node's value is the value of some child

def GameTree.value {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : GameTree N U → N → U

Value of a game tree: a payoff vector. At a Node, the mover selects a child maximizing their own coordinate (argmax over the total preorder).

Computable — with a decidable comparison [DecidableLE U] the argmax is a left fold, so value runs (#eval/decide) on concrete games.

Equations

• (GameTree.Leaf p).value = p
• (GameTree.Node m h t).value = List.argMaxOn (fun (v : N → U) => v m) h.value (GameTree.valueList t)

def GameTree.valueList {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : List (GameTree N U) → List (N → U)

Pointwise image of value over a list of game trees. Structurally recursive on the list.

Equations

• GameTree.valueList [] = []
• GameTree.valueList (x_1 :: xs) = x_1.value :: GameTree.valueList xs

@[simp]

theorem GameTree.value_Leaf {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (p : N → U) : (Leaf p).value = p

@[simp]

theorem GameTree.value_Node {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (m : N) (h : GameTree N U) (t : List (GameTree N U)) : (Node m h t).value = List.argMaxOn (fun (v : N → U) => v m) h.value (valueList t)

@[simp]

theorem GameTree.valueList_nil {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] : valueList [] = []

@[simp]

theorem GameTree.valueList_cons {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (x : GameTree N U) (xs : List (GameTree N U)) : valueList (x :: xs) = x.value :: valueList xs

theorem GameTree.valueList_eq_map {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (l : List (GameTree N U)) : valueList l = List.map value l

valueList l is exactly l.map value. Useful for rewriting.

theorem GameTree.mem_valueList_iff {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] {v : N → U} {l : List (GameTree N U)} : v ∈ valueList l ↔ ∃ (c : GameTree N U), c ∈ l ∧ c.value = v

Membership in valueList via membership in the source list.

theorem GameTree.value_Node_ge {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (m : N) (h : GameTree N U) (t : List (GameTree N U)) (c : GameTree N U) (hmem : c ∈ h :: t) : c.value m ≤ (Node m h t).value m

Key optimality lemma: at a Node m h t, the mover m's coordinate of the backward-induction value dominates every child's.

theorem GameTree.value_Node_eq_some_child_value {N : Type u_1} {U : Type u_2} [TotalPreorder U] [DecidableLE U] (m : N) (h : GameTree N U) (t : List (GameTree N U)) : ∃ (c : GameTree N U), c ∈ h :: t ∧ (Node m h t).value = c.value

The value at a node is itself the value of some child (the argmax). Specifically, argMaxOn ... ∈ value h :: valueList t, so it equals value c for some c ∈ h :: t.