EconCSLib.GameTheory.ExtensiveGame.StochasticGameTree

Finite perfect-information game trees with explicit chance nodes.

This module intentionally keeps stochastic trees separate from the existing no-chance GameTree type. Chance nodes carry rational weights on a nonempty finite successor list; the local probability-sum condition is a predicate rather than a constructor field, so the recursive data type stays lightweight.

Main definitions

• StochasticGameTree — terminal, player, and chance nodes.
• StochasticGameTree.ChanceProbabilitiesSumToOne — local probability check.
• StochasticGameTree.Strategy — pure contingent plans at player nodes.
• StochasticGameTree.expectedPayoffWithFuel — executable fuel-bounded expected-payoff evaluator.
• StochasticGameTree.expectedPayoff — expected payoff using tree-size fuel.
• StochasticGameTree.ofGameTree — embed ordinary no-chance trees.

inductive StochasticGameTree (N : Type u_1) : Type u_1

• Leaf {N : Type u_1} (payoff : N → ℚ) : StochasticGameTree N
• Player {N : Type u_1} (mover : N) (head : StochasticGameTree N) (tail : List (StochasticGameTree N)) : StochasticGameTree N
• Chance {N : Type u_1} (headProb : ℚ) (head : StochasticGameTree N) (tail : List (ℚ × StochasticGameTree N)) : StochasticGameTree N

def StochasticGameTree.Strategy (N : Type u_2) : Type u_2

A pure strategy chooses a child at every player-controlled node.

Equations

• StochasticGameTree.Strategy N = (N → (h : StochasticGameTree N) → (t : List (StochasticGameTree N)) → { c : StochasticGameTree N // c ∈ h :: t })

def StochasticGameTree.headStrategy {N : Type u_1} : Strategy N

The trivial head-selecting strategy, useful for examples that have no strategically relevant player choice.

Equations

• StochasticGameTree.headStrategy x✝¹ h x✝ = ⟨h, ⋯⟩

@[irreducible]

def StochasticGameTree.ofGameTree {N : Type u_1} : GameTree N ℚ → StochasticGameTree N

Embed an ordinary no-chance GameTree into the stochastic tree layer.

Equations

• StochasticGameTree.ofGameTree (GameTree.Leaf p) = StochasticGameTree.Leaf p
• StochasticGameTree.ofGameTree (GameTree.Node m h t) = StochasticGameTree.Player m (StochasticGameTree.ofGameTree h) (List.map StochasticGameTree.ofGameTree t)

def StochasticGameTree.ChanceProbabilitiesSumToOne {N : Type u_1} (headProb : ℚ) (tail : List (ℚ × StochasticGameTree N)) : Prop

Local probability mass check at a chance node.

Equations

• StochasticGameTree.ChanceProbabilitiesSumToOne headProb tail = (headProb + (List.map Prod.fst tail).sum = 1)

noncomputable def StochasticGameTree.expectedPayoffWithFuel {N : Type u_1} (fuel : ℕ) (σ : Strategy N) (g : StochasticGameTree N) (i : N) : ℚ

Fuel-bounded expected payoff under a pure strategy. If fuel runs out, the default payoff is zero; expectedPayoff below supplies tree-size fuel.

Equations

• One or more equations did not get rendered due to their size.
• StochasticGameTree.expectedPayoffWithFuel 0 σ g i = 0
• StochasticGameTree.expectedPayoffWithFuel n.succ σ (StochasticGameTree.Leaf p) i = p i
• StochasticGameTree.expectedPayoffWithFuel n.succ σ (StochasticGameTree.Player m h t) i = StochasticGameTree.expectedPayoffWithFuel n σ (↑(σ m h t)) i

noncomputable def StochasticGameTree.expectedPayoff {N : Type u_1} (σ : Strategy N) (g : StochasticGameTree N) (i : N) : ℚ

Expected payoff with enough fuel for every branch of the finite tree.

Equations

• StochasticGameTree.expectedPayoff σ g i = StochasticGameTree.expectedPayoffWithFuel (sizeOf g) σ g i

def StochasticGameTree.fairCoinGame : StochasticGameTree (Fin 2)

A one-step fair coin game for examples and CI regression checks.

Equations

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

theorem StochasticGameTree.fairCoin_probs_sum_to_one : ChanceProbabilitiesSumToOne (1 / 2) [(1 / 2, Leaf fun (i : Fin 2) => if i = 0 then 0 else 1)]

theorem StochasticGameTree.fairCoin_expected_player0 : expectedPayoff headStrategy fairCoinGame 0 = 1 / 2