LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Covering

Auxiliary declarations for the Borel determinacy formalization.

def GaleStewartGame.Covering.PTrees : Type (u_1 + 1)

a tree that is pruned and nonempty as required for determinacy

Equations

• GaleStewartGame.Covering.PTrees = ((T : Descriptive.Tree.Trees) ×' Descriptive.Tree.IsPruned T.snd ∧ [] ∈ T.snd)

@[simp]

theorem GaleStewartGame.Covering.pTrees_isPruned (T : PTrees) : Descriptive.Tree.IsPruned T.fst.snd

@[simp]

theorem GaleStewartGame.Covering.pTrees_ne (T : PTrees) : [] ∈ T.fst.snd

noncomputable def GaleStewartGame.ResStrategy.chooseSucc {k m : ℕ} {p : Player} {T : Covering.PTrees} (S : ResStrategy T.fst p k) : ResStrategy T.fst p m

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.chooseSucc x hp x✝ = if h' : (↑x).length ≤ k then S x hp h' else Classical.choice ⋯

@[simp]

theorem GaleStewartGame.ResStrategy.res_chooseSucc {k m : ℕ} {p : Player} {T : Covering.PTrees} (S : ResStrategy T.fst p k) (h : k ≤ m) : res h S.chooseSucc = S

theorem GaleStewartGame.ResStrategy.res_surjective {k m : ℕ} {p : Player} {T : Covering.PTrees} (h : m ≤ k) : Function.Surjective (res h)

noncomputable def GaleStewartGame.ResStrategy.chooseSystem {k : ℕ} {p : Player} {T : Covering.PTrees} (S : ResStrategy T.fst p k) : StrategySystem T.fst p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.chooseSystem = { str := fun (k_1 : ℕ) => S.chooseSucc, con := ⋯ }

@[simp]

theorem GaleStewartGame.ResStrategy.chooseSystem_str {k : ℕ} {p : Player} {T : Covering.PTrees} (S : ResStrategy T.fst p k) (k✝ : ℕ) : S.chooseSystem.str k✝ = S.chooseSucc

theorem GaleStewartGame.ResStrategy.chooseSystem_self {k : ℕ} {p : Player} {T : Covering.PTrees} (S : ResStrategy T.fst p k) : S.chooseSystem.str k = S

theorem GaleStewartGame.ResStrategy.str_surjective {k : ℕ} {p : Player} {T : Covering.PTrees} : Function.Surjective fun (S : StrategySystem T.fst p) => S.str k

structure GaleStewartGame.Covering.PTreesS : Type 1

Auxiliary declaration for the Borel determinacy formalization.

• tree : PTrees

  Auxiliary declaration for the Borel determinacy formalization.

structure GaleStewartGame.Covering.LvlStratHom (T U : PTreesS) : Type

a map of strategies whose output on the first k levels only depends on the input on the first k levels

• toFun (p : Player) (k : ℕ) : ResStrategy T.tree.fst p k → ResStrategy U.tree.fst p k

  Auxiliary declaration for the Borel determinacy formalization.

• con (p : Player) {k m : ℕ} (h : m ≤ k) (S : ResStrategy T.tree.fst p k) : ResStrategy.res h (self.toFun p k S) = self.toFun p m (ResStrategy.res h S)

theorem GaleStewartGame.Covering.LvlStratHom.ext {T U : PTreesS} {x y : LvlStratHom T U} (toFun : x.toFun = y.toFun) : x = y

theorem GaleStewartGame.Covering.LvlStratHom.ext_iff {T U : PTreesS} {x y : LvlStratHom T U} : x = y ↔ x.toFun = y.toFun

def GaleStewartGame.Covering.LvlStratHom.id (T : PTreesS) : LvlStratHom T T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.LvlStratHom.id T = { toFun := fun (p : GaleStewartGame.Player) (k : ℕ) => id, con := ⋯ }

def GaleStewartGame.Covering.LvlStratHom.comp {T U V : PTreesS} (g : LvlStratHom U V) (f : LvlStratHom T U) : LvlStratHom T V

Auxiliary declaration for the Borel determinacy formalization.

Equations

• g.comp f = { toFun := fun (p : GaleStewartGame.Player) (k : ℕ) => g.toFun p k ∘ f.toFun p k, con := ⋯ }

@[implicit_reducible]

instance GaleStewartGame.Covering.instCategoryPTreesS : CategoryTheory.Category.{0, 1} PTreesS

Equations

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

@[simp]

theorem GaleStewartGame.Covering.LvlStratHom.id_toFun {k : ℕ} {p : Player} (T : PTreesS) : (CategoryTheory.CategoryStruct.id T).toFun p k = _root_.id

@[simp]

theorem GaleStewartGame.Covering.LvlStratHom.comp_toFun {k : ℕ} {p : Player} {T U V : PTreesS} (f : T ⟶ U) (g : U ⟶ V) : (CategoryTheory.CategoryStruct.comp f g).toFun p k = g.toFun p k ∘ f.toFun p k

theorem GaleStewartGame.Covering.LvlStratHom.ext' {T U : PTreesS} {f g : T ⟶ U} (h : f.toFun = g.toFun) : f = g

theorem GaleStewartGame.Covering.LvlStratHom.ext'_iff {T U : PTreesS} {f g : T ⟶ U} : f = g ↔ f.toFun = g.toFun

def GaleStewartGame.Covering.LvlStratHom.system (p : Player) : CategoryTheory.Functor PTreesS Type

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[reducible, inline]

abbrev GaleStewartGame.Covering.LvlStratHom.systemToObj {p : Player} {T : PTreesS} (S : StrategySystem T.tree.fst p) : (system p).obj T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.LvlStratHom.systemToObj S = cast ⋯ S

@[reducible, inline]

abbrev GaleStewartGame.Covering.LvlStratHom.systemOfObj {p : Player} {T : PTreesS} (S : (system p).obj T) : StrategySystem T.tree.fst p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.LvlStratHom.systemOfObj S = cast ⋯ S

def GaleStewartGame.Covering.LvlStratHom.global (p : Player) : CategoryTheory.Functor PTreesS Type

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[reducible, inline]

abbrev GaleStewartGame.Covering.LvlStratHom.globalToObj {p : Player} {T : PTreesS} (S : Strategy T.tree.fst.snd p) : (global p).obj T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.LvlStratHom.globalToObj S = cast ⋯ S

@[reducible, inline]

abbrev GaleStewartGame.Covering.LvlStratHom.globalOfObj {p : Player} {T : PTreesS} (S : (global p).obj T) : Strategy T.tree.fst.snd p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.LvlStratHom.globalOfObj S = cast ⋯ S

def GaleStewartGame.Covering.bodyLiftExists {T U : PTrees} (toHom : T.fst ⟶ U.fst) (str : { tree := T } ⟶ { tree := U }) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.Covering.bodyLiftExists_iff_system {T U : PTrees} (toHom : T.fst ⟶ U.fst) (str : { tree := T } ⟶ { tree := U }) : bodyLiftExists toHom str ↔ ∀ {p : Player} {S : StrategySystem T.fst p} (y : bodySystem.obj U.fst), consistent y (LvlStratHom.systemOfObj ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map str)) (LvlStratHom.systemToObj S))) → ∃ (x : bodySystem.obj T.fst), consistent x S ∧ (CategoryTheory.ConcreteCategory.hom (bodySystem.map toHom)) x = y

structure GaleStewartGame.Covering (T U : Covering.PTrees) : Type

a covering used in the proof of Borel determinacy, given by a length preserving map of nodes and a map of strategies and satisfying a lifting condition on plays consistent with the strategy

• toHom : T.fst ⟶ U.fst

  Auxiliary declaration for the Borel determinacy formalization.

• str : { tree := T } ⟶ { tree := U }

  Auxiliary declaration for the Borel determinacy formalization.

• h_body : bodyLiftExists self.toHom self.str

theorem GaleStewartGame.Covering.ext {T U : PTrees} {x y : Covering T U} (toHom : x.toHom = y.toHom) (str : x.str = y.str) : x = y

theorem GaleStewartGame.Covering.ext_iff {T U : PTrees} {x y : Covering T U} : x = y ↔ x.toHom = y.toHom ∧ x.str = y.str

@[implicit_reducible]

instance GaleStewartGame.Covering.instCategoryPTrees : CategoryTheory.Category.{0, 1} PTrees

Equations

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

def GaleStewartGame.Covering.PTreeForget : CategoryTheory.Functor PTrees Descriptive.Tree.Trees

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem GaleStewartGame.Covering.id_covering_toHom (T : PTrees) : (CategoryTheory.CategoryStruct.id T).toHom = CategoryTheory.CategoryStruct.id T.fst

@[simp]

theorem GaleStewartGame.Covering.id_covering_str (T : PTrees) : (CategoryTheory.CategoryStruct.id T).str = CategoryTheory.CategoryStruct.id { tree := T }

@[simp]

theorem GaleStewartGame.Covering.comp_covering_toHom {T U V : PTrees} (f : T ⟶ U) (g : U ⟶ V) : (CategoryTheory.CategoryStruct.comp f g).toHom = CategoryTheory.CategoryStruct.comp f.toHom g.toHom

@[simp]

theorem GaleStewartGame.Covering.comp_covering_str {T U V : PTrees} (f : T ⟶ U) (g : U ⟶ V) : (CategoryTheory.CategoryStruct.comp f g).str = CategoryTheory.CategoryStruct.comp f.str g.str

theorem GaleStewartGame.Covering.comp_covering_str_apply {k : ℕ} {p : Player} (S T U : PTrees) (f : S ⟶ T) (g : T ⟶ U) (A : ResStrategy { tree := S }.tree.fst p k) : (CategoryTheory.CategoryStruct.comp f g).str.toFun p k A = g.str.toFun p k (f.str.toFun p k A)

theorem GaleStewartGame.Covering.ext' {T U : PTrees} {f g : T ⟶ U} (h1 : f.toHom = g.toHom) (h2 : f.str = g.str) : f = g

theorem GaleStewartGame.Covering.ext'_iff {T U : PTrees} {f g : T ⟶ U} : f = g ↔ f.toHom = g.toHom ∧ f.str = g.str

def GaleStewartGame.Covering.Fixing (k : ℕ) {T U : PTrees} (f : T ⟶ U) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.Fixing k f = ∃ (x : Descriptive.Tree.Fixing k f.toHom), ∀ (p : GaleStewartGame.Player), f.str.toFun p k = GaleStewartGame.ResStrategy.fromMap f.toHom ⋯

@[simp]

theorem GaleStewartGame.Covering.fixing_id (k : ℕ) (T : PTrees) : Fixing k (CategoryTheory.CategoryStruct.id T)

theorem GaleStewartGame.Covering.fixing_comp (k : ℕ) {T U V : PTrees} (f : T ⟶ U) (g : U ⟶ V) (hf : Fixing k f) (hg : Fixing k g) : Fixing k (CategoryTheory.CategoryStruct.comp f g)

theorem GaleStewartGame.Covering.fixing_snd_mon {k m : ℕ} (hm : k ≤ m) {T U : PTrees} (f : T ⟶ U) (h : Fixing m f) (p : Player) : f.str.toFun p k = ResStrategy.fromMap f.toHom ⋯

theorem GaleStewartGame.Covering.fixing_mon {k n : ℕ} {S T : PTrees} (f : S ⟶ T) (h : Fixing k f) (hn : n ≤ k) : Fixing n f

def GaleStewartGame.Covering.Games : Type (u_1 + 1)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.Covering.Games = ((A : Type ?u.1) ×' (G : GaleStewartGame.Game A) ×' Descriptive.Tree.IsPruned G.tree ∧ [] ∈ G.tree)

@[simp]

theorem GaleStewartGame.Covering.games_isPruned (G : Games) : Descriptive.Tree.IsPruned G.snd.fst.tree

@[simp]

theorem GaleStewartGame.Covering.games_ne (G : Games) : [] ∈ G.snd.fst.tree

@[implicit_reducible]

instance GaleStewartGame.Covering.instTopologicalSpaceFstPSigmaGameAndIsPrunedTreeMemListSubtypeSetCompleteSublatticeTreeNil (G : Games) : TopologicalSpace G.fst

Equations

• GaleStewartGame.Covering.instTopologicalSpaceFstPSigmaGameAndIsPrunedTreeMemListSubtypeSetCompleteSublatticeTreeNil G = ⊥

instance GaleStewartGame.Covering.instDiscreteTopologyFstPSigmaGameAndIsPrunedTreeMemListSubtypeSetCompleteSublatticeTreeNil (G : Games) : DiscreteTopology G.fst

@[reducible, inline]

abbrev GaleStewartGame.Covering.Games.tree (G : Games) : PTrees

Auxiliary declaration for the Borel determinacy formalization.

Equations

• G.tree = ⟨⟨G.fst, G.snd.fst.tree⟩, ⋯⟩

structure GaleStewartGame.Covering.Games.Covering (G' G : Games) extends GaleStewartGame.Covering G'.tree G.tree : Type

Auxiliary declaration for the Borel determinacy formalization.

• toHom : G'.tree.fst ⟶ G.tree.fst
• str : { tree := G'.tree } ⟶ { tree := G.tree }
• h_body : bodyLiftExists self.toHom self.str
• hpre : ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map self.toHom)) ⁻¹' G.snd.fst.payoff = G'.snd.fst.payoff

theorem GaleStewartGame.Covering.Games.Covering.ext_iff {G' G : Games} {x y : G'.Covering G} : x = y ↔ x.toHom = y.toHom ∧ x.str = y.str

theorem GaleStewartGame.Covering.Games.Covering.ext {G' G : Games} {x y : G'.Covering G} (toHom : x.toHom = y.toHom) (str : x.str = y.str) : x = y

theorem GaleStewartGame.Covering.covering_hpre_pl {G' G : Games} (f : G'.Covering G) (p : Player) : ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map f.toHom)) ⁻¹' p.payoff G.snd.fst = p.payoff G'.snd.fst

theorem GaleStewartGame.Covering.covering_winning {G' G : Games} (f : G'.Covering G) {p : Player} {S : Strategy G'.tree.fst.snd p} (h : S.pre.IsWinning) : (LvlStratHom.globalOfObj ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.global p).map f.str)) (LvlStratHom.globalToObj S))).pre.IsWinning

def GaleStewartGame.Covering.Games.IsUnravelable (G : Games) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• G.IsUnravelable = ∀ (k : ℕ), ∃ (G' : GaleStewartGame.Covering.Games) (f : G'.Covering G), GaleStewartGame.Covering.Fixing k f.toCovering ∧ IsClopen G'.snd.fst.payoff

theorem GaleStewartGame.Covering.Games.IsUnravelable.isDetermined {G : Games} (h : G.IsUnravelable) : G.snd.fst.IsDetermined