LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Strat

Auxiliary declarations for the Borel determinacy formalization.

noncomputable def GaleStewartGame.BorelDet.One.stratMap {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (lvl : ℕ) (R : ResStrategy (gameAsTrees hyp) Player.one lvl) : ResStrategy (oldAsTrees hyp) Player.one lvl

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

noncomputable def GaleStewartGame.BorelDet.One.stratMap' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (R : Strategy (gameTree hyp) Player.one) : Strategy G.tree Player.one

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.One.stratMap' R x hp = GaleStewartGame.BorelDet.One.stratMap (↑x).length ((GaleStewartGame.strategyEquivSystem R).str (↑x).length) x hp ⋯

theorem GaleStewartGame.BorelDet.One.stratMap'_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (R : Strategy (gameTree hyp) Player.one) (x : ↥G.tree) (hp : IsPosition (↑x) Player.one) (hx : (↑x).length ≤ 2 * k) : stratMap' R x hp = ResStrategy.fromMap (treeHom hyp) ⋯ ((strategyEquivSystem R).str (↑x).length) x hp ⋯

structure GaleStewartGame.BorelDet.One.TreeLift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) : Type u_1

Auxiliary declaration for the Borel determinacy formalization.

• R : Strategy (gameTree hyp) Player.one

  Auxiliary declaration for the Borel determinacy formalization.

• x : ↥(stratMap' self.R).pre.subtree

  Auxiliary declaration for the Borel determinacy formalization.

• hlvl : 2 * k < (↑self.x).length

theorem GaleStewartGame.BorelDet.One.TreeLift.ext {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : TreeLift hyp} (R : x.R = y.R) : x.x ≍ y.x → x = y

theorem GaleStewartGame.BorelDet.One.TreeLift.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : TreeLift hyp} : x = y ↔ x.R = y.R ∧ x.x ≍ y.x

theorem GaleStewartGame.BorelDet.One.TreeLift.ext' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : TreeLift hyp} (hR : H.R = H'.R) (hx : ↑H.x = ↑H'.x) : H = H'

theorem GaleStewartGame.BorelDet.One.TreeLift.ext'_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : TreeLift hyp} : H = H' ↔ H.R = H'.R ∧ ↑H.x = ↑H'.x

theorem GaleStewartGame.BorelDet.One.TreeLift.hlvl_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : 2 * k + 1 ≤ (↑H.x).length

Auxiliary declaration for the Borel determinacy formalization.

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.hlvl' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : 2 * k ≤ (↑H.x).length

def GaleStewartGame.BorelDet.One.TreeLift.preLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.preLift = { x := (GaleStewartGame.BorelDet.One.stratMap' H.R).pre.subtreeIncl H.x, hlvl := ⋯, R := (GaleStewartGame.strategyEquivSystem H.R).str (2 * k + 1) }

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.preLift_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : H.preLift.R = (strategyEquivSystem H.R).str (2 * k + 1)

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.preLift_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : ↑H.preLift.x = ↑H.x

def GaleStewartGame.BorelDet.One.TreeLift.take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (n : ℕ) (hk : 2 * k < n) : TreeLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.take n hk = { R := H.R, x := Descriptive.Tree.take n H.x, hlvl := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.take_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (n : ℕ) (hk : 2 * k < n) : (H.take n hk).x = Descriptive.Tree.take n H.x

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.take_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (n : ℕ) (hk : 2 * k < n) : (H.take n hk).R = H.R

theorem GaleStewartGame.BorelDet.One.TreeLift.take_of_length_le {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) {h : 2 * k < n} (h' : (↑H.x).length ≤ n) : H.take n h = H

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : H.take (↑H.x).length ⋯ = H

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.take_trans {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hm : 2 * k < m) (hn : 2 * k < n) : (H.take m hm).take n hn = H.take (min m n) ⋯

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.preLift_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hk : 2 * k < n) : (H.take n hk).preLift = H.preLift.take n hk

Auxiliary declaration for the Borel determinacy formalization.

noncomputable def GaleStewartGame.BorelDet.One.TreeLift.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hp : IsPosition (↑H.preLift.x) Player.one) : Descriptive.Tree.ExtensionsAt H.preLift.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.extension hp = H.preLift.extension hp ((GaleStewartGame.strategyEquivSystem H.R).str (↑H.preLift.x).length)

theorem GaleStewartGame.BorelDet.One.TreeLift.extension_val_congr {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : TreeLift hyp} (h : H = H') {hp : IsPosition (↑H.preLift.x) Player.one} : ↑(H.extension hp) = ↑(H'.extension ⋯)

theorem GaleStewartGame.BorelDet.One.TreeLift.stratMap'_extend {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : stratMap' H.R ((stratMap' H.R).pre.subtreeIncl H.x) = H.extension

def GaleStewartGame.BorelDet.One.TreeLift.dropLast {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : TreeLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.dropLast h = H.take ((↑H.x).length - 1) ⋯

theorem GaleStewartGame.BorelDet.One.TreeLift.dropLast_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : (H.dropLast h).R = H.R

theorem GaleStewartGame.BorelDet.One.TreeLift.dropLast_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : ↑(H.dropLast h).x = List.take ((↑H.x).length - 1) ↑H.x

@[simp]

theorem GaleStewartGame.BorelDet.One.TreeLift.dropLast_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} : (H.dropLast h).x = Descriptive.Tree.take ((↑H.x).length - 1) H.x

theorem GaleStewartGame.BorelDet.One.TreeLift.x_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) (hp : IsPosition (↑H.x) Player.zero) : (↑H.x)[(↑H.x).length - 1] = ↑((H.dropLast h).extension ⋯)

theorem GaleStewartGame.BorelDet.One.TreeLift.x_mem_tree' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) (hp : IsPosition (↑H.x) Player.zero) : H.preLift.x = ((H.dropLast h).extension ⋯).valT'

theorem GaleStewartGame.BorelDet.One.TreeLift.pInv_fixing {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : n ≤ 2 * k) : Descriptive.Tree.Fixing (↑((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x))).length (treeHom hyp)

theorem GaleStewartGame.BorelDet.One.TreeLift.pInv_isPosition {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : n ≤ 2 * k) {p : Player} (hp : IsPosition (List.take n ↑H.x) p) : IsPosition (↑(Descriptive.Tree.pInv (treeHom hyp) ((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x)) ⋯)) p

theorem GaleStewartGame.BorelDet.One.TreeLift.pInv_fixing_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : Descriptive.Tree.Fixing (↑(Descriptive.Tree.take (2 * k) ((stratMap' H.R).pre.subtreeIncl H.x))).length (treeHom hyp)

theorem GaleStewartGame.BorelDet.One.TreeLift.losable_or_winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) : H.preLift.Losable ∨ H.preLift.Winnable

theorem GaleStewartGame.BorelDet.One.TreeLift.x_mem_tree_short' {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : n < 2 * k) (hp : IsPosition (List.take n ↑H.x) Player.one) : Descriptive.Tree.take (n + 1) (Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) ((stratMap' H.R).pre.subtreeIncl H.x)) ⋯) = (H.R (Descriptive.Tree.pInv (treeHom hyp) ((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x)) ⋯) ⋯).valT'

theorem GaleStewartGame.BorelDet.One.TreeLift.x_mem_tree_short {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : n < 2 * k) (hp : IsPosition (List.take n ↑H.x) Player.one) : (pInvTreeHomMap hyp (List.take (2 * k) ↑H.x))[n] = ↑(H.R (Descriptive.Tree.pInv (treeHom hyp) ((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x)) ⋯) ⋯)

theorem GaleStewartGame.BorelDet.One.TreeLift.get_eq_get_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hn : n < (↑H.x).length) (hk : 2 * k ≤ n) : (↑H.x)[n] = (↑(H.take (n + 1) ⋯).x)[(↑(H.take (n + 1) ⋯).x).length - 1]

theorem GaleStewartGame.BorelDet.One.TreeLift.wLift_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : H.preLift.Won) : h.lift'.liftVal ∈ H.R.pre.subtree

theorem GaleStewartGame.BorelDet.One.TreeLift.lLift_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : H.preLift.Losable) : h.lift'.liftVal ∈ H.R.pre.subtree

theorem GaleStewartGame.BorelDet.One.TreeLift.take_winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : H.preLift.Winnable) (n : ℕ) : (H.take (2 * k + 1 + PreStrategy.WinningPrefix.num h + n) ⋯).preLift.Winnable

theorem GaleStewartGame.BorelDet.One.TreeLift.winnable_subtree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hL : H.preLift.Winnable) (hnL : ¬∃ (h : 2 * k + 2 ≤ (↑H.x).length), (H.dropLast h).preLift.Won) : List.drop (2 * k + 1 + PreStrategy.WinningPrefix.num hL) ↑H.x ∈ (PreStrategy.WinningPrefix.strat hL).pre.subtree

def GaleStewartGame.BorelDet.One.bodyTake {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) : TreeLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.One.bodyTake y n = { R := R, x := Descriptive.Tree.body.take (2 * k + 1 + n) y, hlvl := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.bodyTake_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) : (bodyTake y n).x = Descriptive.Tree.body.take (2 * k + 1 + n) y

@[simp]

theorem GaleStewartGame.BorelDet.One.bodyTake_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) : (bodyTake y n).R = R

@[simp]

theorem GaleStewartGame.BorelDet.One.bodyTake_take {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : 2 * k + 1 ≤ m) : (bodyTake y n).take m ⋯ = bodyTake y (min (m - (2 * k + 1)) n)

theorem GaleStewartGame.BorelDet.One.takeLift_mono {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) : (bodyTake y m).preLift ≤ (bodyTake y n).preLift ↔ m ≤ n

@[simp]

theorem GaleStewartGame.BorelDet.One.takeLift_wonPos {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) : (bodyTake y n).preLift.WonPos = (bodyTake y 0).preLift.WonPos

@[simp]

theorem GaleStewartGame.BorelDet.One.takeLift_game {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) : (bodyTake y n).preLift.game = (bodyTake y 0).preLift.game

theorem GaleStewartGame.BorelDet.One.won_of_winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) (h : (bodyTake y n).preLift.Winnable) : ∃ (m : ℕ), (bodyTake y m).preLift.Won

noncomputable def GaleStewartGame.BorelDet.One.wonLift {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : (bodyTake y n).preLift.Won) : ↑(Descriptive.Tree.body R.pre.subtree)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.BorelDet.One.wonLift_map {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : (bodyTake y n).preLift.Won) : ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map π)) ⟨↑(wonLift y h), ⋯⟩) = ↑y

noncomputable def GaleStewartGame.BorelDet.One.lostLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : ∀ (n : ℕ), (bodyTake y n).preLift.Losable) : ↑(Descriptive.Tree.body R.pre.subtree)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.BorelDet.One.lostLift_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : ∀ (n : ℕ), (bodyTake y n).preLift.Losable) : ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map π)) ⟨↑(lostLift y h), ⋯⟩) = ↑y

theorem GaleStewartGame.BorelDet.One.body_stratMap {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.one} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) : ∃ (x : ↑(Descriptive.Tree.body R.pre.subtree)), ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map π)) ⟨↑x, ⋯⟩) = ↑y