Stopping time

For p q : Player and x : LGame, stoppingTime p q x : WithTop NatOrdinal is called the stopping time of x, and represents how long it will take with optimal play for p for force a win if it is q's turn to move on x. No move by p can strictly decrease the stopping time, and no move by -p can strictly increase the stopping time. If p cannot force a win then it takes the value ⊤, and -p can survive forever by only moving to other positions whose stopping time is also ⊤. Otherwise it is an ordinal that strictly decreases whenever -p moves. Then p can force a win by moving to positions with an equal stopping time. The stopping times of the positions for -p will then spell out a strictly decreasing sequence of ordinals, which must eventually reach 0, at which point -p will have no moves left. The lemma stoppingTime_of_eq characterizes the behavior of stoppingTime when it is p's turn to move, and the lemma stoppingTime_of_ne characterizes the behavior of stoppingTime when it is -p's turn to move.

stoppingTime p : Player → LGame.{u} → WithTop NatOrdinal.{u} is the unique fixed point of the map val ↦ fun q x ↦ if p = q then ⨅ y ∈ x.moves q, val (-q) y else ⨆ y ∈ x.moves q, val (-q) y + 1. It therefore satisfies both an induction and a coinduction principle, given by stoppingTime_induction and stoppingTime_coinduction. stoppingTime_induction says that any other val : Player → LGame → WithTop NatOrdinal decreased by this map must be bigger than stoppingTime, and stoppingTime_coinduction says that any other val : Player → LGame → WithTop NatOrdinal increased by this map must be smaller than stoppingTime.

For Mathlib

theorem Monotone.iInf' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Monotone (f i)) : Monotone fun (x : α) => ⨅ (i : ι), f i x

theorem Monotone.iSup' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [Preorder α] [CompleteLattice β] {f : ι → α → β} (hf : ∀ (i : ι), Monotone (f i)) : Monotone fun (x : α) => ⨆ (i : ι), f i x

theorem Order.lt_add_one_iff_not_isMax {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) : x < x + 1 ↔ ¬IsMax x

theorem Order.le_add_one {α : Type u_1} [Preorder α] [Add α] [One α] [SuccAddOrder α] (x : α) : x ≤ x + 1

@[irreducible]

def LGame.stoppingTime (p q : Player) (x : LGame) : WithTop NatOrdinal

stoppingTime p q x is the time it takes for p to force a win if q goes first on x, counted in moves made by -p.

Equations

• LGame.stoppingTime p q x = if p = q then OrderHom.lfp (LGame.stoppingTimeApprox✝ p) x else ⨆ i ∈ LGame.moves q x, OrderHom.lfp (LGame.stoppingTimeApprox✝¹ p) i + 1

theorem LGame.stoppingTime_of_eq {p q : Player} (h : p = q) (x : LGame) : stoppingTime p q x = ⨅ y ∈ moves q x, stoppingTime p (-q) y

theorem LGame.stoppingTime_of_ne {p q : Player} (h : p ≠ q) (x : LGame) : stoppingTime p q x = ⨆ y ∈ moves q x, stoppingTime p (-q) y + 1

theorem LGame.stoppingTime_induction (p : Player) (val : Player → LGame → WithTop NatOrdinal) (hp : ∀ (x : LGame), ⨅ y ∈ moves p x, val (-p) y ≤ val p x) (hnp : ∀ (x : LGame), ⨆ y ∈ moves (-p) x, val p y + 1 ≤ val (-p) x) : stoppingTime p ≤ val

theorem LGame.stoppingTime_coinduction (p : Player) (val : Player → LGame → WithTop NatOrdinal) (hp : ∀ (x : LGame), val p x ≤ ⨅ y ∈ moves p x, val (-p) y) (hnp : ∀ (x : LGame), val (-p) x ≤ ⨆ y ∈ moves (-p) x, val p y + 1) : val ≤ stoppingTime p