LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BuildLevelwise

Auxiliary declarations for the Borel determinacy formalization.

structure GaleStewartGame.BodySystemObj (T : Descriptive.Tree.Trees) : Type u_1

Auxiliary declaration for the Borel determinacy formalization.

• res (k : ℕ) : (Descriptive.Tree.resEq k).obj T

  Auxiliary declaration for the Borel determinacy formalization.

• con (k : ℕ) : ↑(self.res k) <+: ↑(self.res (k + 1))

theorem GaleStewartGame.BodySystemObj.ext {T : Descriptive.Tree.Trees} {x y : BodySystemObj T} (res : x.res = y.res) : x = y

theorem GaleStewartGame.BodySystemObj.ext_iff {T : Descriptive.Tree.Trees} {x y : BodySystemObj T} : x = y ↔ x.res = y.res

@[simp]

theorem GaleStewartGame.bodySystem_con' {k m : ℕ} {T : Descriptive.Tree.Trees} (x : BodySystemObj T) : ↑(x.res k) <+: ↑(x.res m) ↔ k ≤ m

@[simp]

theorem GaleStewartGame.bodySystem_take_val {k m : ℕ} {T : Descriptive.Tree.Trees} (x : BodySystemObj T) : List.take m ↑(x.res k) = ↑(x.res (min k m))

@[simp]

theorem GaleStewartGame.bodySystem_take {k m : ℕ} {T : Descriptive.Tree.Trees} (x : BodySystemObj T) : Descriptive.Tree.take m (Descriptive.Tree.resEq.val' (x.res k)) = Descriptive.Tree.resEq.val' (x.res (min k m))

theorem GaleStewartGame.bodySystem_take' {k m : ℕ} {T : Descriptive.Tree.Trees} (x : BodySystemObj T) (h : m ≤ k) : List.take m ↑(x.res k) = ↑(x.res m)

def GaleStewartGame.bodySystem : CategoryTheory.Functor Descriptive.Tree.Trees (Type u_1)

an isomorph of bodyFunctor that is more convenient to build levelwise

Equations

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

@[simp]

theorem GaleStewartGame.bodySystem_obj (T : Descriptive.Tree.Trees) : bodySystem.obj T = BodySystemObj T

@[reducible, inline]

abbrev GaleStewartGame.BodySystemObj.toObj {T : Descriptive.Tree.Trees} (x : BodySystemObj T) : bodySystem.obj T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• x.toObj = cast ⋯ x

@[reducible, inline]

abbrev GaleStewartGame.BodySystemObj.ofObj {T : Descriptive.Tree.Trees} (x : bodySystem.obj T) : BodySystemObj T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BodySystemObj.ofObj x = cast ⋯ x

theorem GaleStewartGame.BodySystemObj.obj_ext {T : Descriptive.Tree.Trees} {x y : bodySystem.obj T} (h : ofObj x = ofObj y) : x = y

theorem GaleStewartGame.BodySystemObj.obj_ext_iff {T : Descriptive.Tree.Trees} {x y : bodySystem.obj T} : x = y ↔ ofObj x = ofObj y

def GaleStewartGame.bodyEquivSystemApp (T : Descriptive.Tree.Trees) : ↑(Descriptive.Tree.body T.snd) ≃ BodySystemObj T

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem GaleStewartGame.bodyEquivSystemApp_symm_apply_coe (T : Descriptive.Tree.Trees) (x : BodySystemObj T) (n : ℕ) : ↑((bodyEquivSystemApp T).symm x) n = (↑(x.res (n + 1))).get ⟨n, ⋯⟩

@[simp]

theorem GaleStewartGame.bodyEquivSystemApp_apply_res_coe (T : Descriptive.Tree.Trees) (x : ↑(Descriptive.Tree.body T.snd)) (k : ℕ) : ↑(((bodyEquivSystemApp T) x).res k) = Stream'.take k ↑x

noncomputable def GaleStewartGame.bodyEquivSystem : Descriptive.Tree.bodyFunctor ≅ bodySystem

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.bodyEquivSystem_hom_app_hom_apply_res_coe (X : Descriptive.Tree.Trees) (a✝ : Descriptive.Tree.bodyFunctor.obj X) (k : ℕ) : ↑(((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.hom.app X)) a✝).res k) = Stream'.take k ↑((CategoryTheory.eqToIso ⋯).hom.hom'.toFun a✝)

theorem GaleStewartGame.bodyEquivSystem_inv_app_hom_apply_coe (X : Descriptive.Tree.Trees) (a✝ : bodySystem.obj X) (n : ℕ) : ↑((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.inv.app X)) a✝) n = (↑(((CategoryTheory.eqToIso ⋯).inv.hom'.toFun a✝).res (n + 1)))[n]

theorem GaleStewartGame.bodyEquivSystem_hom_app_res_coe {k : ℕ} {T : Descriptive.Tree.Trees} (x : Descriptive.Tree.bodyFunctor.obj T) : ↑((BodySystemObj.ofObj ((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.hom.app T)) x)).res k) = Stream'.take k ↑x

@[reducible, inline]

abbrev GaleStewartGame.BodySystemObj.contains {T : Descriptive.Tree.Trees} (x : BodySystemObj T) (y : List T.fst) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• x.contains y = (y = ↑(x.res y.length))

@[reducible, inline]

abbrev GaleStewartGame.BodySystemObj.containsTree {T : Descriptive.Tree.Trees} (x : BodySystemObj T) (y : ↑↑T.snd) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• x.containsTree y = (y = Descriptive.Tree.resEq.val' (x.res (↑y).length))

theorem GaleStewartGame.BodySystemObj.bodySystem_contains_iff {T : Descriptive.Tree.Trees} (x : BodySystemObj T) (y : ↑↑T.snd) : x.contains ↑y ↔ x.containsTree y

theorem GaleStewartGame.BodySystemObj.bodySystem_contains_iff' {T : Descriptive.Tree.Trees} (x : BodySystemObj T) {z : ↥T.snd} (y : Descriptive.Tree.ExtensionsAt z) : x.contains y.val' ↔ x.containsTree y.valT'

theorem GaleStewartGame.BodySystemObj.res_val_congr {m n : ℕ} {T : Descriptive.Tree.Trees} (x y : BodySystemObj T) (h : x = y) (h' : m = n) : ↑(x.res m) = ↑(y.res n)

theorem GaleStewartGame.BodySystemObj.res_val'_congr {m n : ℕ} {T : Descriptive.Tree.Trees} (x y : BodySystemObj T) (h : x = y) (h' : m = n) : Descriptive.Tree.resEq.val' (x.res m) = Descriptive.Tree.resEq.val' (y.res n)

theorem GaleStewartGame.BodySystemObj.containsTree.map {S T : Descriptive.Tree.Trees} {x : BodySystemObj S} {y : ↑↑S.snd} (h : x.containsTree y) (f : S ⟶ T) : (ofObj ((CategoryTheory.ConcreteCategory.hom (bodySystem.map f)) x.toObj)).containsTree ((CategoryTheory.ConcreteCategory.hom f) y)

@[simp]

theorem GaleStewartGame.IsPosition.iff_lenHom (p : Player) {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (x : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) S) : IsPosition (↑((CategoryTheory.ConcreteCategory.hom f) x)) p ↔ IsPosition (↑x) p

@[simp]

theorem GaleStewartGame.iff_pInv_lenHom (p : Player) {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (x : ↑↑T.snd) (h : Descriptive.Tree.Fixing (↑x).length f) : IsPosition (↑(Descriptive.Tree.pInv f x h)) p ↔ IsPosition (↑x) p

def GaleStewartGame.ResStrategy (T : Descriptive.Tree.Trees) (p : Player) (k : ℕ) : Type u_1

a strategy defined only on positions up to length k

Equations

• GaleStewartGame.ResStrategy T p k = ((x : ↑↑T.snd) → GaleStewartGame.IsPosition (↑x) p → (↑x).length ≤ k → Descriptive.Tree.ExtensionsAt x)

theorem GaleStewartGame.ResStrategy.ext {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} {S S' : ResStrategy T p k} (h : ∀ (x : ↑↑T.snd) (hp : IsPosition (↑x) p) (hl : (↑x).length ≤ k), S x hp hl = S' x hp hl) : S = S'

theorem GaleStewartGame.ResStrategy.ext_iff {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} {S S' : ResStrategy T p k} : S = S' ↔ ∀ (x : ↑↑T.snd) (hp : IsPosition (↑x) p) (hl : (↑x).length ≤ k), S x hp hl = S' x hp hl

theorem GaleStewartGame.ResStrategy.eval_val'_congr' {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (S S' : ResStrategy T p k) (h : S = S') (x x' : ↑↑T.snd) (h' : x = x') (hp : IsPosition (↑x) p) (hl : (↑x).length ≤ k) : (S x hp hl).val' = (S' x' ⋯ ⋯).val'

theorem GaleStewartGame.ResStrategy.eval_valT'_congr' {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (S S' : ResStrategy T p k) (h : S = S') (x x' : ↑↑T.snd) (h' : x = x') (hp : IsPosition (↑x) p) (hl : (↑x).length ≤ k) : (S x hp hl).valT' = (S' x' ⋯ ⋯).valT'

theorem GaleStewartGame.ResStrategy.eval_val_congr' {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (S S' : ResStrategy T p k) (h : S = S') (x x' : ↑↑T.snd) (h' : x = x') (hp : IsPosition (↑x) p) (hl : (↑x).length ≤ k) : ↑(S x hp hl) = ↑(S' x' ⋯ ⋯)

def GaleStewartGame.ResStrategy.res {k m : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (h : m ≤ k) (S : ResStrategy T p k) : ResStrategy T p m

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.ResStrategy.res h S x hp hl = S x hp ⋯

@[simp]

theorem GaleStewartGame.ResStrategy.res_refl {k : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (S : ResStrategy T p k) : res ⋯ S = S

@[simp]

theorem GaleStewartGame.ResStrategy.res_trans {T : Descriptive.Tree.Trees} {p : Player} (m n k : ℕ) (S : ResStrategy T p k) (mn : m ≤ n) (nk : n ≤ k) : res mn (res nk S) = res ⋯ S

noncomputable def GaleStewartGame.ResStrategy.fromMap {k : ℕ} {S T : Descriptive.Tree.Trees} {p : Player} (f : S ⟶ T) (h : Descriptive.Tree.Fixing k f := by as_aux_lemma => synthFixing) (S' : ResStrategy S p k) : ResStrategy T p k

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.ResStrategy.fromMap f h S' x hx hl = Descriptive.Tree.ExtensionsAt.map f ⋯ (S' (Descriptive.Tree.pInv f x ⋯) ⋯ ⋯)

theorem GaleStewartGame.ResStrategy.fromMap_congr {k : ℕ} {S T : Descriptive.Tree.Trees} {p : Player} {f g : S ⟶ T} (heq : f = g) (hh : Descriptive.Tree.Fixing k f) : fromMap f hh = fromMap g ⋯

noncomputable def GaleStewartGame.ResStrategy.fromMapInv {k : ℕ} {S T : Descriptive.Tree.Trees} {p : Player} (f : S ⟶ T) (h : Descriptive.Tree.Fixing (k + 1) f := by as_aux_lemma => synthFixing) (S' : ResStrategy T p k) : ResStrategy S p k

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.ResStrategy.fromMapInv f h S' y hy hl = (Descriptive.Tree.extensionsEquiv f y ⋯).symm (S' ((CategoryTheory.ConcreteCategory.hom f) y) ⋯ ⋯)

noncomputable def GaleStewartGame.ResStrategy.fromMapEquiv {S T : Descriptive.Tree.Trees} (p : Player) (k : ℕ) (f : S ⟶ T) (h : Descriptive.Tree.Fixing (k + 1) f := by as_aux_lemma => synthFixing) : ResStrategy S p k ≃ ResStrategy T p k

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.ResStrategy.fromMapEquiv p k f h = { toFun := GaleStewartGame.ResStrategy.fromMap f ⋯, invFun := GaleStewartGame.ResStrategy.fromMapInv f ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem GaleStewartGame.ResStrategy.res_fromMap {S T : Descriptive.Tree.Trees} {p : Player} {k m : ℕ} (h : m ≤ k) (f : S ⟶ T) (hf : Descriptive.Tree.Fixing k f) (S' : ResStrategy S p k) : res h (fromMap f hf S') = fromMap f ⋯ (res h S')

@[simp]

theorem GaleStewartGame.ResStrategy.fromMap_id {T : Descriptive.Tree.Trees} {p : Player} (k : ℕ) (S' : ResStrategy T p k) : fromMap (CategoryTheory.CategoryStruct.id T) ⋯ S' = S'

@[simp]

theorem GaleStewartGame.ResStrategy.fromMap_comp {p : Player} (k : ℕ) {S T U : Descriptive.Tree.Trees} (f : S ⟶ T) (g : T ⟶ U) (hf : Descriptive.Tree.Fixing k f := by as_aux_lemma => synthFixing) (hg : Descriptive.Tree.Fixing k g := by as_aux_lemma => synthFixing) (S' : ResStrategy S p k) : fromMap (CategoryTheory.CategoryStruct.comp f g) ⋯ S' = fromMap g hg (fromMap f hf S')

theorem GaleStewartGame.ResStrategy.fromMap_comp' {p : Player} (k : ℕ) {S T U : Descriptive.Tree.Trees} (f : S ⟶ T) (g : T ⟶ U) (hf : Descriptive.Tree.Fixing k f) (hg : Descriptive.Tree.Fixing k g) (S' : ResStrategy S p k) : fromMap (CategoryTheory.CategoryStruct.comp f g) ⋯ S' = fromMap g hg (fromMap f hf S')

@[simp]

theorem GaleStewartGame.ResStrategy.fromMap_valT' {k : ℕ} {p : Player} {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (hf : Descriptive.Tree.Fixing k f) (S' : ResStrategy S p k) (x : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) S) (hx : IsPosition (↑x) p) (hl : (↑x).length ≤ k) : (fromMap f hf S' ((CategoryTheory.ConcreteCategory.hom f) x) ⋯ ⋯).valT' = (CategoryTheory.ConcreteCategory.hom f) (S' x hx hl).valT'

structure GaleStewartGame.StrategySystem (T : Descriptive.Tree.Trees) (p : Player) : Type u_1

a strategy as an inverse limit of a sequence of ResStrategy

• str (k : ℕ) : ResStrategy T p k

  Auxiliary declaration for the Borel determinacy formalization.

• con (k : ℕ) : ResStrategy.res ⋯ (self.str (k + 1)) = self.str k

theorem GaleStewartGame.StrategySystem.ext_iff {T : Descriptive.Tree.Trees} {p : Player} {x y : StrategySystem T p} : x = y ↔ x.str = y.str

theorem GaleStewartGame.StrategySystem.ext {T : Descriptive.Tree.Trees} {p : Player} {x y : StrategySystem T p} (str : x.str = y.str) : x = y

@[simp]

theorem GaleStewartGame.StrategySystem.con' {k m : ℕ} {T : Descriptive.Tree.Trees} {p : Player} (S : StrategySystem T p) (h : k ≤ m) : ResStrategy.res h (S.str m) = S.str k

def GaleStewartGame.strategyEquivSystem {T : Descriptive.Tree.Trees} {p : Player} : Strategy T.snd p ≃ StrategySystem T p

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem GaleStewartGame.strategyEquivSystem_symm_apply {T : Descriptive.Tree.Trees} {p : Player} (S : StrategySystem T p) (x : ↥T.snd) (hp : IsPosition (↑x) p) : strategyEquivSystem.symm S x hp = S.str (↑x).length x hp ⋯

@[simp]

theorem GaleStewartGame.strategyEquivSystem_apply_str {T : Descriptive.Tree.Trees} {p : Player} (S : Strategy T.snd p) (x✝ : ℕ) (x : ↑↑T.snd) (h : IsPosition (↑x) p) (x✝¹ : (↑x).length ≤ x✝) : (strategyEquivSystem S).str x✝ x h x✝¹ = S x h

theorem GaleStewartGame.preStrategy_body {p : Player} {A : Type u_1} {T : ↥(Descriptive.tree A)} {y : Stream' A} (f : PreStrategy T p) : y ∈ Descriptive.Tree.body f.subtree ↔ ∃ (hy : y ∈ Descriptive.Tree.body T), ∀ (x : ↥T) (hp : IsPosition (↑x) p) (hb : y ∈ Stream'.Discrete.principalOpen ↑x), ⟨y.get (↑x).length, ⋯⟩ ∈ f x hp

theorem GaleStewartGame.strategy_body {p : Player} {A : Type u_1} {T : ↥(Descriptive.tree A)} {y : Stream' A} (f : Strategy T p) : y ∈ Descriptive.Tree.body f.pre.subtree ↔ y ∈ Descriptive.Tree.body T ∧ ∀ (x : ↥T) (hp : IsPosition (↑x) p), y ∈ Stream'.Discrete.principalOpen ↑x → y.get (↑x).length = ↑(f x hp)

def GaleStewartGame.consistent {T : Descriptive.Tree.Trees} {p : Player} (x : bodySystem.obj T) (S : StrategySystem T p) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.mem_principalOpen_iff_bodySystem_contains {T : Descriptive.Tree.Trees} (x : List T.fst) (y : ↑(Descriptive.Tree.body T.snd)) : ↑y ∈ Stream'.Discrete.principalOpen x ↔ (BodySystemObj.ofObj ((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.hom.app T)) y)).contains x

theorem GaleStewartGame.bodyEquivSystem_strat {T : Descriptive.Tree.Trees} {p : Player} {x : (fun (X : Type u_1) => X) (Descriptive.Tree.bodyFunctor.obj T)} (S : StrategySystem T p) : ↑x ∈ Descriptive.Tree.body (strategyEquivSystem.symm S).pre.subtree ↔ consistent ((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.hom.app T)) x) S

theorem GaleStewartGame.bodyEquivSystem_strat' {T : Descriptive.Tree.Trees} {p : Player} {x : (fun (X : Type u_1) => X) (bodySystem.obj T)} (S : StrategySystem T p) : ↑((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.inv.app T)) x) ∈ Descriptive.Tree.body (strategyEquivSystem.symm S).pre.subtree ↔ consistent x S

theorem GaleStewartGame.bodyEquivSystem_strat'' {T : Descriptive.Tree.Trees} {p : Player} {x : (fun (X : Type u_1) => X) (Descriptive.Tree.bodyFunctor.obj T)} (S : Strategy T.snd p) : ↑x ∈ Descriptive.Tree.body S.pre.subtree ↔ consistent ((CategoryTheory.ConcreteCategory.hom (bodyEquivSystem.hom.app T)) x) (strategyEquivSystem S)