EconCSLib.GameTheory.ExtensiveGame.BehaviorStrategy

Behavior-strategy primitives for the Arena-based extensive-game framework.

This file starts the infrastructure needed for MSZ Theorem 7.5. The probabilistic definitions are fuel-indexed so they fit the current Arena framework, which supports both finite and infinite games.

Main definitions

• ExtensiveGame.BehaviorStrategy - a player chooses a probability distribution over actions at each state they control.
• ExtensiveGame.BehaviorProfile - one behavior strategy for each player.
• ExtensiveGame.BehaviorStrategy.IsCompletelyMixed - every available action at a controlled state receives positive probability.
• ExtensiveGame.BehaviorProfile.probAt - probability assigned to an action at a player-controlled state.
• ExtensiveGame.reachProb - finite-fuel probability of reaching a state.
• ExtensiveGame.expectedPayoff - finite-fuel expected payoff under a behavior profile.
• ExtensiveGame.BehaviorProfile.deviate - unilateral behavior-strategy deviations.
• ExtensiveGame.ReachedSubgamePayoffTransfer - affine payoff-transfer data for a positively reached subgame.
• ExtensiveGame.IsBehaviorNashEq - finite-fuel behavioral Nash equilibrium.
• ExtensiveGame.BehaviorProfile.restrictSubgame - restriction to subgameAt.
• ExtensiveGame.BehaviorProfile.liftReachableSubgame - local lift of reachable-subgame deviations, preserving the baseline profile outside the reached subgame.

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Definition 7.6 and Theorem 7.5.

Subgame simp lemmas

@[simp]

theorem ExtensiveGame.subgameAt_init {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (s : G.State) : (G.subgameAt s).init = s

@[simp]

theorem ExtensiveGame.subgameAt_mover {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (s t : G.State) : (G.subgameAt s).mover t = G.mover t

@[simp]

theorem ExtensiveGame.subgameAt_payoff {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (s t : G.State) (i : iota) : (G.subgameAt s).payoff t i = G.payoff t i

@[simp]

theorem ExtensiveGame.subgameAt_next {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (s t : G.State) (a : G.Action t) : (G.subgameAt s).next t a = G.next t a

@[implicit_reducible]

instance ExtensiveGame.subgameAt_action_fintype {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (root : G.State) [inst : (s : G.State) → Fintype (G.Action s)] (s : (G.subgameAt root).State) : Fintype ((G.subgameAt root).Action s)

Equations

• G.subgameAt_action_fintype root = inst

@[implicit_reducible]

instance ExtensiveGame.subgameAt_isEmpty_decidable {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (root : G.State) [inst : (s : G.State) → Decidable (IsEmpty (G.Action s))] (s : (G.subgameAt root).State) : Decidable (IsEmpty ((G.subgameAt root).Action s))

Equations

• G.subgameAt_isEmpty_decidable root = inst

@[implicit_reducible]

instance ExtensiveGame.reachableSubgameAt_action_fintype {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (root : G.State) [inst : (s : G.State) → Fintype (G.Action s)] (s : (G.reachableSubgameAt root).State) : Fintype ((G.reachableSubgameAt root).Action s)

Equations

• G.reachableSubgameAt_action_fintype root s = inst ↑s

@[implicit_reducible]

instance ExtensiveGame.reachableSubgameAt_isEmpty_decidable {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (root : G.State) [inst : (s : G.State) → Decidable (IsEmpty (G.Action s))] (s : (G.reachableSubgameAt root).State) : Decidable (IsEmpty ((G.reachableSubgameAt root).Action s))

Equations

• G.reachableSubgameAt_isEmpty_decidable root s = inst ↑s

Behavior strategies

def ExtensiveGame.BehaviorStrategy {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) (i : iota) [(s : G.State) → Fintype (G.Action s)] : Type (max u_4 u_3)

A behavior strategy for player i: at every nonterminal state controlled by i, choose a probability distribution over the actions available there.

This is a state-based primitive. A later imperfect-information layer can impose the usual information-set consistency condition by requiring equal distributions across states in the same information set.

The nonterminal premise prevents a semantically ignored terminal mover label from creating an impossible simplex coordinate over an empty action type.

Equations

• G.BehaviorStrategy i = ((s : G.State) → G.mover s = some i → ¬G.isTerminal s → ↑(stdSimplex ℝ (G.Action s)))

def ExtensiveGame.BehaviorProfile {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) [(s : G.State) → Fintype (G.Action s)] : Type (max (max u_1 u_4) u_3)

A behavior-strategy profile: one behavior strategy for every player.

Equations

• G.BehaviorProfile = ((i : iota) → G.BehaviorStrategy i)

Complete mixing

def ExtensiveGame.BehaviorStrategy.IsCompletelyMixed {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} (beta : G.BehaviorStrategy i) : Prop

A behavior strategy is completely mixed if every available action at every state controlled by the player receives positive probability.

This is the state-based behavior-strategy part of MSZ Definition 7.6. The later imperfect-information layer can identify states inside the same information set; this predicate is already the local full-support condition used by the current Arena-based behavior-strategy API.

Equations

• beta.IsCompletelyMixed = ∀ (s : G.State) (h : G.mover s = some i) (hnonterminal : ¬G.isTerminal s) (a : G.Action s), 0 < ↑(beta s h hnonterminal) a

Complete mixing

def ExtensiveGame.BehaviorProfile.IsCompletelyMixed {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) : Prop

A behavior profile is completely mixed if each player's behavior strategy is completely mixed.

Equations

• beta.IsCompletelyMixed = ∀ (i : iota), (beta i).IsCompletelyMixed

theorem ExtensiveGame.BehaviorProfile.IsCompletelyMixed.player {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {beta : G.BehaviorProfile} (hbeta : beta.IsCompletelyMixed) (i : iota) : (beta i).IsCompletelyMixed

A completely mixed behavior profile gives a completely mixed behavior strategy for each player.

def ExtensiveGame.BehaviorProfile.probAt {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) {s : G.State} {i : iota} (h : G.mover s = some i) (a : G.Action s) : ℝ

The probability that a behavior profile assigns to action a at a state controlled by player i.

Equations

• beta.probAt h a = ↑(beta i s h ⋯) a

def ExtensiveGame.BehaviorProfile.actionProb {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (s : G.State) (a : G.Action s) : ℝ

The action probability induced by a behavior profile at a state.

At a player-controlled state this reads the controlling player's behavior strategy. At a chance state it returns 0; this placeholder is compatible with the NoChance layer and can be replaced by explicit chance probabilities in a later stochastic layer.

Equations

• beta.actionProb s a = match h : G.mover s with | some i => ↑(beta i s h ⋯) a | none => 0

theorem ExtensiveGame.BehaviorProfile.actionProb_nonneg {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (s : G.State) (a : G.Action s) : 0 ≤ beta.actionProb s a

A behavior profile assigns nonnegative probability to every action.

theorem ExtensiveGame.BehaviorProfile.IsCompletelyMixed.actionProb_pos {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {beta : G.BehaviorProfile} (hbeta : beta.IsCompletelyMixed) {s : G.State} {i : iota} (hm : G.mover s = some i) (a : G.Action s) : 0 < beta.actionProb s a

At player-controlled states, a completely mixed behavior profile gives positive probability to every available action.

Deviations

def ExtensiveGame.BehaviorProfile.deviate {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) (beta' : G.BehaviorStrategy who) : G.BehaviorProfile

Unilateral deviation of a behavior profile: player who switches to beta', while every other player keeps the original behavior strategy.

Equations

• beta.deviate who beta' = Function.update beta who beta'

@[simp]

theorem ExtensiveGame.BehaviorProfile.deviate_same {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) (beta' : G.BehaviorStrategy who) : beta.deviate who beta' who = beta'

@[simp]

theorem ExtensiveGame.BehaviorProfile.deviate_of_ne {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) (beta' : G.BehaviorStrategy who) {other : iota} (h : other ≠ who) : beta.deviate who beta' other = beta other

Subgame restriction

def ExtensiveGame.BehaviorStrategy.restrictSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} (beta : G.BehaviorStrategy i) (root : G.State) : (G.subgameAt root).BehaviorStrategy i

Restrict a behavior strategy to the subgame rooted at root.

Since subgameAt keeps the same state space, actions, and movers, this is just the same local action distribution viewed from the subgame.

Equations

• beta.restrictSubgame root s h hnonterminal = beta s h hnonterminal

theorem ExtensiveGame.BehaviorStrategy.restrictSubgame_eq_self {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} (beta : G.BehaviorStrategy i) (root : G.State) : beta.restrictSubgame root = beta

def ExtensiveGame.BehaviorStrategy.liftSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} {root : G.State} (beta : (G.subgameAt root).BehaviorStrategy i) : G.BehaviorStrategy i

View a behavior strategy for a subgame as a behavior strategy for the original game.

This is well-typed because subgameAt keeps the same state space, actions, and movers; it only changes the initial state.

Equations

• beta.liftSubgame s h hnonterminal = beta s h hnonterminal

theorem ExtensiveGame.BehaviorStrategy.liftSubgame_eq_self {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} {root : G.State} (beta : (G.subgameAt root).BehaviorStrategy i) : beta.liftSubgame = beta

@[simp]

theorem ExtensiveGame.BehaviorStrategy.restrictSubgame_liftSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} {root : G.State} (beta : (G.subgameAt root).BehaviorStrategy i) : beta.liftSubgame.restrictSubgame root = beta

Reachable-state subgame restriction

def ExtensiveGame.BehaviorStrategy.restrictReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} (beta : G.BehaviorStrategy i) (root : G.State) : (G.reachableSubgameAt root).BehaviorStrategy i

Restrict a behavior strategy to the subtype subgame consisting only of states reachable from root.

Equations

• beta.restrictReachableSubgame root s h hnonterminal = beta (↑s) h hnonterminal

def ExtensiveGame.BehaviorStrategy.liftReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} {root : G.State} [(s : G.State) → Decidable (G.Reachable root s)] (base : G.BehaviorStrategy i) (beta : (G.reachableSubgameAt root).BehaviorStrategy i) : G.BehaviorStrategy i

Lift a reachable-subgame behavior strategy to the original game, preserving the baseline strategy outside the reachable subgame.

Equations

• base.liftReachableSubgame beta s h hnonterminal = if hs : G.Reachable root s then beta ⟨s, hs⟩ h hnonterminal else base s h hnonterminal

@[simp]

theorem ExtensiveGame.BehaviorStrategy.restrictReachableSubgame_liftReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {i : iota} {root : G.State} [(s : G.State) → Decidable (G.Reachable root s)] (base : G.BehaviorStrategy i) (beta : (G.reachableSubgameAt root).BehaviorStrategy i) : (base.liftReachableSubgame beta).restrictReachableSubgame root = beta

def ExtensiveGame.BehaviorProfile.restrictSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (root : G.State) : (G.subgameAt root).BehaviorProfile

Restrict a behavior profile to the subgame rooted at root.

Equations

• beta.restrictSubgame root i = (beta i).restrictSubgame root

theorem ExtensiveGame.BehaviorProfile.restrictSubgame_eq_self {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (root : G.State) : beta.restrictSubgame root = beta

def ExtensiveGame.BehaviorProfile.liftSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {root : G.State} (beta : (G.subgameAt root).BehaviorProfile) : G.BehaviorProfile

View a behavior profile for a subgame as a behavior profile for the original game.

Equations

• beta.liftSubgame i = (beta i).liftSubgame

@[simp]

theorem ExtensiveGame.BehaviorProfile.restrictSubgame_liftSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {root : G.State} (beta : (G.subgameAt root).BehaviorProfile) : beta.liftSubgame.restrictSubgame root = beta

def ExtensiveGame.BehaviorProfile.restrictReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (root : G.State) : (G.reachableSubgameAt root).BehaviorProfile

Restrict a behavior profile to the subtype subgame of states reachable from root.

Equations

• beta.restrictReachableSubgame root i = (beta i).restrictReachableSubgame root

def ExtensiveGame.BehaviorProfile.liftReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {root : G.State} [(s : G.State) → Decidable (G.Reachable root s)] (base : G.BehaviorProfile) (beta : (G.reachableSubgameAt root).BehaviorProfile) : G.BehaviorProfile

Lift a reachable-subgame behavior profile to the original game, preserving the baseline profile outside the reachable subgame.

Equations

• base.liftReachableSubgame beta i = (base i).liftReachableSubgame (beta i)

@[simp]

theorem ExtensiveGame.BehaviorProfile.restrictReachableSubgame_liftReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] {root : G.State} [(s : G.State) → Decidable (G.Reachable root s)] (base : G.BehaviorProfile) (beta : (G.reachableSubgameAt root).BehaviorProfile) : (base.liftReachableSubgame beta).restrictReachableSubgame root = beta

theorem ExtensiveGame.BehaviorProfile.restrictReachableSubgame_deviate_liftReachableSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] {root : G.State} [(s : G.State) → Decidable (G.Reachable root s)] (beta : G.BehaviorProfile) (who : iota) (beta' : (G.reachableSubgameAt root).BehaviorStrategy who) : (beta.deviate who ((beta who).liftReachableSubgame beta')).restrictReachableSubgame root = (beta.restrictReachableSubgame root).deviate who beta'

A reachable-subgame deviation can be lifted to an original-game deviation that changes the deviating player only below root.

@[simp]

theorem ExtensiveGame.BehaviorProfile.actionProb_restrictSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (root s : G.State) (a : G.Action s) : (beta.restrictSubgame root).actionProb s a = beta.actionProb s a

theorem ExtensiveGame.BehaviorProfile.restrictSubgame_deviate {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) (beta' : G.BehaviorStrategy who) (root : G.State) : (beta.deviate who beta').restrictSubgame root = (beta.restrictSubgame root).deviate who (beta'.restrictSubgame root)

Restricting a deviated behavior profile to a subgame is the same as restricting first and then applying the corresponding deviation inside the subgame.

theorem ExtensiveGame.BehaviorProfile.restrictSubgame_deviate_liftSubgame {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [(s : G.State) → Fintype (G.Action s)] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) {root : G.State} (beta' : (G.subgameAt root).BehaviorStrategy who) : (beta.deviate who beta'.liftSubgame).restrictSubgame root = (beta.restrictSubgame root).deviate who beta'

A subgame deviation can be lifted to an original-game deviation whose restriction to the subgame is the intended subgame deviation.

Reach probabilities

noncomputable def ExtensiveGame.reachProbFrom {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (start target : G.State) : ℕ → ℝ

Finite-fuel probability of reaching target from start under a behavior profile.

The definition records the probability of hitting target within the remaining fuel. It is intentionally fuel-indexed, matching ExtensiveGame.Play, because the Arena framework also supports infinite games.

Equations

• One or more equations did not get rendered due to their size.
• ExtensiveGame.reachProbFrom beta start target 0 = if start = target then 1 else 0

noncomputable def ExtensiveGame.reachProb {iota : Type u_1} {U : Type u_2} (G : ExtensiveGame iota U) [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (target : G.State) (fuel : ℕ) : ℝ

Finite-fuel probability of reaching target from the initial state.

Equations

• G.reachProb beta target fuel = ExtensiveGame.reachProbFrom beta G.init target fuel

def ExtensiveGame.BehaviorProfile.IsCompletelyMixedWithPositiveReach {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] (beta : G.BehaviorProfile) (fuel : ℕ) : Prop

Completely mixed behavior together with the current positive-reach interface for every subgame root at a fixed fuel.

In finite games with explicit positive chance probabilities, the second component follows from complete mixing and reachability of every game-tree vertex. The Arena behavior layer currently keeps chance probabilities and finite-depth bounds abstract, so Corollary 7.7 uses this as the precise bridge from complete mixing to the positive-reach hypothesis of Theorem 7.5.

Equations

• beta.IsCompletelyMixedWithPositiveReach fuel = (beta.IsCompletelyMixed ∧ ∀ (root : G.State), 0 < G.reachProb beta root fuel)

theorem ExtensiveGame.BehaviorProfile.IsCompletelyMixedWithPositiveReach.mixed {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] {beta : G.BehaviorProfile} {fuel : ℕ} (hbeta : beta.IsCompletelyMixedWithPositiveReach fuel) : beta.IsCompletelyMixed

The complete-mixing component of IsCompletelyMixedWithPositiveReach.

theorem ExtensiveGame.BehaviorProfile.IsCompletelyMixedWithPositiveReach.reach_pos {iota : Type u_1} {U : Type u_2} {G : ExtensiveGame iota U} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] {beta : G.BehaviorProfile} {fuel : ℕ} (hbeta : beta.IsCompletelyMixedWithPositiveReach fuel) (root : G.State) : 0 < G.reachProb beta root fuel

The positive-reach component of IsCompletelyMixedWithPositiveReach.

Expected payoff

noncomputable def ExtensiveGame.expectedPayoffFrom {iota : Type u_1} {G : ExtensiveGame iota ℝ} [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] (beta : G.BehaviorProfile) (start : G.State) : ℕ → iota → ℝ

Finite-fuel expected payoff from start under a behavior profile.

If the fuel runs out, or if a terminal state is reached, the current state's payoff is used. At a chance state without explicit chance probabilities, the current payoff is also used; the intended no-chance use case rules out nonterminal chance states by assuming NoChance G.

Equations

• One or more equations did not get rendered due to their size.
• ExtensiveGame.expectedPayoffFrom beta start 0 x✝ = G.payoff start x✝

noncomputable def ExtensiveGame.expectedPayoff {iota : Type u_1} (G : ExtensiveGame iota ℝ) [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] (beta : G.BehaviorProfile) (fuel : ℕ) (who : iota) : ℝ

Finite-fuel expected payoff from the initial state under a behavior profile.

Equations

• G.expectedPayoff beta fuel who = ExtensiveGame.expectedPayoffFrom beta G.init fuel who

@[simp]

theorem ExtensiveGame.expectedPayoffFrom_restrictSubgame {iota : Type u_1} {G : ExtensiveGame iota ℝ} [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] (beta : G.BehaviorProfile) (root start : G.State) (fuel : ℕ) (who : iota) : expectedPayoffFrom (beta.restrictSubgame root) start fuel who = expectedPayoffFrom beta start fuel who

@[simp]

theorem ExtensiveGame.expectedPayoff_restrictSubgame_init {iota : Type u_1} {G : ExtensiveGame iota ℝ} [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] (beta : G.BehaviorProfile) (fuel : ℕ) (who : iota) : (G.subgameAt G.init).expectedPayoff (beta.restrictSubgame G.init) fuel who = G.expectedPayoff beta fuel who

theorem ExtensiveGame.expectedPayoff_restrictSubgame_deviate_liftSubgame {iota : Type u_1} {G : ExtensiveGame iota ℝ} [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] (beta : G.BehaviorProfile) (who : iota) {root : G.State} (beta' : (G.subgameAt root).BehaviorStrategy who) (fuel : ℕ) : (G.subgameAt root).expectedPayoff ((beta.deviate who beta'.liftSubgame).restrictSubgame root) fuel who = (G.subgameAt root).expectedPayoff ((beta.restrictSubgame root).deviate who beta') fuel who

The subgame payoff of a lifted original-game deviation agrees with the payoff of the corresponding subgame deviation.

def ExtensiveGame.ReachedSubgamePayoffTransfer {iota : Type u_1} (G : ExtensiveGame iota ℝ) [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] (beta : G.BehaviorProfile) (root : G.State) (fuel : ℕ) : Prop

Payoff-transfer data for a subgame reached with positive probability.

This is the numerical decomposition used in the proof of MSZ Theorem 7.5: for each subgame deviation, the original-game payoff can be written as a common outside term plus a positive scale times the payoff in the reached subgame. Later finite-history probability work can prove this interface from the concrete definition of reachProb and expected payoffs.

Equations

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

theorem ExtensiveGame.ReachedSubgamePayoffTransfer.init {iota : Type u_1} (G : ExtensiveGame iota ℝ) [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] (beta : G.BehaviorProfile) (fuel : ℕ) : G.ReachedSubgamePayoffTransfer beta G.init fuel

The payoff-transfer interface holds trivially for the root subgame.

Behavioral Nash equilibrium

def ExtensiveGame.IsBehaviorNashEq {iota : Type u_1} (G : ExtensiveGame iota ℝ) [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] (beta : G.BehaviorProfile) (fuel : ℕ) : Prop

A finite-fuel behavioral Nash equilibrium: no player can improve their finite-fuel expected payoff by a unilateral behavior-strategy deviation.

Equations

• G.IsBehaviorNashEq beta fuel = ∀ (who : iota) (beta' : G.BehaviorStrategy who), G.expectedPayoff (beta.deviate who beta') fuel who ≤ G.expectedPayoff beta fuel who

def ExtensiveGame.IsBehaviorSubgamePerfect {iota : Type u_1} (G : ExtensiveGame iota ℝ) [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] (beta : G.BehaviorProfile) (fuel : ℕ) : Prop

A finite-fuel behavioral subgame-perfect equilibrium: at every subgame root, the restricted behavior profile is a finite-fuel behavioral Nash equilibrium of that subgame.

Equations

• G.IsBehaviorSubgamePerfect beta fuel = ∀ (root : G.State), (G.subgameAt root).IsBehaviorNashEq (beta.restrictSubgame root) fuel

theorem ExtensiveGame.IsBehaviorNashEq.restrictSubgame_of_reachProb_pos {iota : Type u_1} {G : ExtensiveGame iota ℝ} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] {beta : G.BehaviorProfile} {root : G.State} {fuel : ℕ} (hNash : G.IsBehaviorNashEq beta fuel) (hreach : 0 < G.reachProb beta root fuel) (hpay : G.ReachedSubgamePayoffTransfer beta root fuel) : (G.subgameAt root).IsBehaviorNashEq (beta.restrictSubgame root) fuel

MSZ Theorem 7.5, finite-fuel behavior-strategy interface form.

If a behavior profile is a Nash equilibrium in the original game, a subgame root is reached with positive probability, and the reached-subgame payoff transfer interface holds, then the restricted behavior profile is a Nash equilibrium of the subgame.

The transfer interface is affine rather than equality-based: the original-game and subgame payoffs share the same outside term and a positive scale, so a profitable subgame deviation would lift to a profitable original-game deviation.

theorem ExtensiveGame.IsBehaviorNashEq.toSubgamePerfect_of_reachProb_pos {iota : Type u_1} {G : ExtensiveGame iota ℝ} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] {beta : G.BehaviorProfile} {fuel : ℕ} (hNash : G.IsBehaviorNashEq beta fuel) (hreach : ∀ (root : G.State), 0 < G.reachProb beta root fuel) (hpay : ∀ (root : G.State), G.ReachedSubgamePayoffTransfer beta root fuel) : G.IsBehaviorSubgamePerfect beta fuel

If every subgame root is reached with positive finite-fuel probability, a behavioral Nash equilibrium restricts to a Nash equilibrium in every subgame.

This packages repeated applications of IsBehaviorNashEq.restrictSubgame_of_reachProb_pos.

theorem ExtensiveGame.IsBehaviorNashEq.toSubgamePerfect_of_isCompletelyMixed {iota : Type u_1} {G : ExtensiveGame iota ℝ} [DecidableEq G.State] [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] {beta : G.BehaviorProfile} {fuel : ℕ} (hNash : G.IsBehaviorNashEq beta fuel) (hbeta : beta.IsCompletelyMixedWithPositiveReach fuel) (hpay : ∀ (root : G.State), G.ReachedSubgamePayoffTransfer beta root fuel) : G.IsBehaviorSubgamePerfect beta fuel

MSZ Corollary 7.7, finite-fuel behavior-strategy interface form.

In the current Arena behavior layer, complete mixing is paired with an explicit positive-reach interface for every subgame root. Under the same affine payoff-transfer interface used by Theorem 7.5, a completely mixed behavioral Nash equilibrium is behavioral subgame-perfect.

theorem ExtensiveGame.IsBehaviorNashEq.restrictSubgame_init {iota : Type u_1} {G : ExtensiveGame iota ℝ} [(s : G.State) → Fintype (G.Action s)] [(s : G.State) → Decidable (IsEmpty (G.Action s))] [DecidableEq iota] {beta : G.BehaviorProfile} {fuel : ℕ} (hNash : G.IsBehaviorNashEq beta fuel) : (G.subgameAt G.init).IsBehaviorNashEq (beta.restrictSubgame G.init) fuel

Root-subgame special case of the restriction theorem.

When the subgame root is the original initial state, no reach-probability decomposition is needed: the subgame is definitionally the same continuation problem with a different subgameAt view.