EconCSLib.GameTheory.ExtensiveGame.Subgame

Subgames in the Arena framework.

In a state-space game, a subgame starting at state s is simply the same game with init := s. The arena (dynamics) doesn't change — only the starting point.

Main definitions

• ExtensiveGame.reachableSubgameAt — the subtype subgame restricted to states reachable from a root.
• ExtensiveGame.subgameAt — the subgame starting at state s

The underlying reachability relation lives in the canonical Execution.Reachability module.

References

• [MSZ] Definition 3.11, Definition 7.2

def ExtensiveGame.subgameAt {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : ExtensiveGame N U

The subgame starting at state s: same arena, different starting point.

Equations

• G.subgameAt s = { toArena := G.toArena, init := s, mover := G.mover, payoff := G.payoff }

theorem ExtensiveGame.subgameAt_arena {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (s : G.State) : (G.subgameAt s).toArena = G.toArena

The arena of a subgame is the same arena.

def ExtensiveGame.reachableSubgameAt {U : Type u_2} {iota : Type u_3} (G : ExtensiveGame iota U) (root : G.State) : ExtensiveGame iota U

The subgame whose state space is restricted to states reachable from root.

The older subgameAt view changes only the initial state. This subtype version is useful when a proof needs to express that deviations are local to the subtree below root.

Equations

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

@[simp]

theorem ExtensiveGame.reachableSubgameAt_init {U : Type u_2} {iota : Type u_3} (G : ExtensiveGame iota U) (root : G.State) : (G.reachableSubgameAt root).init = ⟨root, ⋯⟩

@[simp]

theorem ExtensiveGame.reachableSubgameAt_mover {U : Type u_2} {iota : Type u_3} (G : ExtensiveGame iota U) (root : G.State) (s : (G.reachableSubgameAt root).State) : (G.reachableSubgameAt root).mover s = G.mover ↑s

@[simp]

theorem ExtensiveGame.reachableSubgameAt_payoff {U : Type u_2} {iota : Type u_3} (G : ExtensiveGame iota U) (root : G.State) (s : (G.reachableSubgameAt root).State) (i : iota) : (G.reachableSubgameAt root).payoff s i = G.payoff (↑s) i

@[simp]

theorem ExtensiveGame.reachableSubgameAt_next {U : Type u_2} {iota : Type u_3} (G : ExtensiveGame iota U) (root : G.State) (s : (G.reachableSubgameAt root).State) (a : (G.reachableSubgameAt root).Action s) : (G.reachableSubgameAt root).next s a = ⟨G.next (↑s) a, ⋯⟩