LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.GaleStewart

Auxiliary declarations for the Borel determinacy formalization.

#Closed determinacy

This file proves the Gale-Stewart lemma on the determinacy of closed games. More precisely, the defensive strategy is winning for closed games.

theorem GaleStewartGame.PreStrategy.cast_quasi {A : Type u_1} {T T' : ↥(Descriptive.tree A)} {p p' : Player} (hT : T = T') (hP : p = p') (S : PreStrategy T p) : (cast ⋯ S).IsQuasi ↔ S.IsQuasi

theorem GaleStewartGame.PreStrategy.cast_winning {A : Type u_1} {p : Player} {G G' : Game A} (h : G = G') (S : PreStrategy G.tree p) : (cast ⋯ S).IsWinning ↔ S.IsWinning

theorem GaleStewartGame.Game.defensive_equals_pre {A : Type u_1} {G : Game A} {p : Player} (hP : Descriptive.Tree.IsPruned G.tree) (h : ¬G.ExistsWinning p.swap) : (G.defensiveQuasi p hP).fst.subtree = (G.defensivePre p).subtree

theorem GaleStewartGame.Game.isClosed_image_payoff {A : Type u_1} {G : Game A} : IsClosed G.payoff ↔ IsClosed (Subtype.val '' G.payoff)

theorem GaleStewartGame.Game.defensive_winning_isClosed {A : Type u_1} {G : Game A} (hC : IsClosed G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) : (G.defensivePre Player.zero).IsWinning

theorem GaleStewartGame.Game.defensive_winning_isOpen {A : Type u_1} {G : Game A} (hC : IsOpen G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) : (G.defensivePre Player.one).IsWinning

theorem GaleStewartGame.Game.gale_stewart_precise {A : Type u_1} {G : Game A} (h : IsClosed G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) (h' : ¬G.ExistsWinning Player.one) : (G.defensiveQuasi Player.zero hP).fst.IsWinning

theorem GaleStewartGame.Game.gale_stewart {A : Type u_1} {G : Game A} (h : IsClosed G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) : G.IsDetermined

theorem GaleStewartGame.Game.gale_stewart_precise' {A : Type u_1} {G : Game A} (h : IsOpen G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) (h' : ¬∃ (S : Strategy G.tree Player.zero), S.pre.IsWinning) : (G.defensiveQuasi Player.one hP).fst.IsWinning