LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.TreeLift #

Auxiliary declarations for the Borel determinacy formalization.

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

ResStrategy (oldAsTrees hyp) Player.zero lvl

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

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

Strategy G.tree Player.zero

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.stratMap'_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (R : Strategy (gameTree hyp) Player.zero) (x : ↥G.tree) (hp : IsPosition (↑x) Player.zero) (hx : (↑x).length ≤ 2 * k) :

stratMap' R x hp = ResStrategy.fromMap (treeHom hyp) ⋯ ((strategyEquivSystem R).str (↑x).length) x hp ⋯

source

structure GaleStewartGame.BorelDet.Zero.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.zero
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

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.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

source

theorem GaleStewartGame.BorelDet.Zero.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

source

theorem GaleStewartGame.BorelDet.Zero.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'

source

theorem GaleStewartGame.BorelDet.Zero.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

source

theorem GaleStewartGame.BorelDet.Zero.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.

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.TreeLift.hlvl' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

2 * k ≤ (↑H.x).length

source

def GaleStewartGame.BorelDet.Zero.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.Zero.stratMap' H.R).pre.subtreeIncl H.x, hlvl := ⋯, R := (GaleStewartGame.strategyEquivSystem H.R).str (2 * k) }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.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)

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.TreeLift.preLift_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

↑H.preLift.x = ↑H.x

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.pInv_fixing {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : TreeLift hyp) (h : n ≤ 2 * k) :

Descriptive.Tree.Fixing (↑((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x))).length (treeHom hyp)

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.pInv_isPosition {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (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

source

theorem GaleStewartGame.BorelDet.Zero.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)

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.pInv_isPosition_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

IsPosition (↑(Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) ((stratMap' H.R).pre.subtreeIncl H.x)) ⋯)) Player.zero

source

def GaleStewartGame.BorelDet.Zero.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 := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.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

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.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

source

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

H.take n h = H

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.TreeLift.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

H.take (↑H.x).length ⋯ = H

source

@[simp]

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

(H.take m hm).take n hn = H.take (min m n) ⋯

source

@[simp]

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

(H.take n hk).preLift = H.preLift.take n hk

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.conShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

H.preLift.ConShort

source

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

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.lift h = { toPreLift := H.preLift, h'lvl := h, conShort := ⋯ }

Instances For

source

@[simp]

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

(H.lift h).toPreLift = H.preLift

source

noncomputable def GaleStewartGame.BorelDet.Zero.TreeLift.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hp : IsPosition (↑H.x) Player.zero) :

Descriptive.Tree.ExtensionsAt (H.lift ⋯).x

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extension hp = (H.lift ⋯).extension hp ((GaleStewartGame.strategyEquivSystem H.R).str (↑(H.lift ⋯).x).length)

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.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.x) Player.zero} :

↑(H.extension hp) = ↑(H'.extension ⋯)

source

@[simp]

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

(H.take n hk).lift h' = (H.lift ⋯).take n ⋯

source

theorem GaleStewartGame.BorelDet.Zero.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

source

def GaleStewartGame.BorelDet.Zero.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) ⋯

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.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

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.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

source

theorem GaleStewartGame.BorelDet.Zero.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.one) :

(↑H.x)[(↑H.x).length - 1] = ↑((H.dropLast h).extension ⋯)

source

theorem GaleStewartGame.BorelDet.Zero.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.one) :

H.preLift.x = ((H.dropLast h).extension ⋯).valT'

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.conLong_or_lost {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) :

H.preLift.ConLong ∨ ∃ (h : 2 * k + 2 ≤ (↑H.x).length), (H.lift h).Lost

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.lost_of_lost' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : TreeLift hyp} {h : 2 * k + 2 ≤ (↑H.x).length} (hL : (H.lift h).Lost') :

(H.lift h).Lost

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.x_mem_tree_short' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : TreeLift hyp) (h' : 2 * k + 2 ≤ (↑H.x).length) (h : n ≤ 2 * k) (hp : IsPosition (List.take n ↑H.x) Player.zero) :

Descriptive.Tree.take (n + 1) (H.lift h').liftShort = (H.R (Descriptive.Tree.pInv (treeHom hyp) ((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x)) ⋯) ⋯).valT'

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.x_mem_tree_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : TreeLift hyp) (h' : 2 * k + 2 ≤ (↑H.x).length) (h : n ≤ 2 * k) (hp : IsPosition (List.take n ↑H.x) Player.zero) :

(↑(H.lift h').liftShort)[n] = ↑(H.R (Descriptive.Tree.pInv (treeHom hyp) ((stratMap' H.R).pre.subtreeIncl (Descriptive.Tree.take n H.x)) ⋯) ⋯)

source

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

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.WinnableOrLost = ∃ (h : 2 * k + 2 ≤ (↑H.x).length), (H.lift h).Winnable ∨ (H.lift h).Lost

Instances For

source

noncomputable def GaleStewartGame.BorelDet.Zero.TreeLift.wLLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hWL : H.WinnableOrLost) :

WLLift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.wLLift' hWL = if hW : (H.lift ⋯).Winnable then hW.toWLift' else have hL := ⋯; hL.toLLift'

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.TreeLift.wLLift'_to_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hWL : H.WinnableOrLost) :

(H.wLLift' hWL).toLift = H.lift ⋯

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.wLift'_eq_wLLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} (hW : (H.lift h).Winnable) :

hW.toWLift' = H.wLLift' ⋯

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.lLift'_eq_wLLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} (hL : (H.lift h).Lost) :

hL.toLLift' = H.wLLift' ⋯

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.lift_mem_tree_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (hWL : H.WinnableOrLost) (n : ℕ) (hn : n < 2 * k + 1) (hp : IsPosition (↑(Descriptive.Tree.take n (H.wLLift' hWL).lift)) Player.zero) :

(H.wLLift' hWL).liftVal[n] = ↑(H.R (Descriptive.Tree.take n (H.wLLift' hWL).lift) hp)

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.wLift'_eq_wLLift'_long {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} (hW : (H.lift h).Winnable) (hp : IsPosition (↑(Descriptive.Tree.take n hW.toWLift'.lift)) Player.zero) :

↑(H.R (Descriptive.Tree.take n hW.toWLift'.lift) hp) = ↑(H.R (Descriptive.Tree.take n (H.wLLift' ⋯).lift) ⋯)

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.lLift'_eq_wLLift'_long {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} (hL : (H.lift h).Lost) (hp : IsPosition (↑(Descriptive.Tree.take n hL.toLLift'.lift)) Player.zero) :

↑(H.R (Descriptive.Tree.take n hL.toLLift'.lift) hp) = ↑(H.R (Descriptive.Tree.take n (H.wLLift' ⋯).lift) ⋯)

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.get_eq_get_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (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]

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.wLift_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) (hW : (H.lift h).Winnable) :

hW.toWLift'.liftVal ∈ H.R.pre.subtree

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.lLift_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) (hL : (H.lift h).Lost) :

hL.toLLift'.liftVal ∈ H.R.pre.subtree

source

theorem GaleStewartGame.BorelDet.Zero.TreeLift.losable_subtree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : TreeLift hyp) {h : 2 * k + 2 ≤ (↑H.x).length} (hL : (H.lift h).Losable) (hnL : ¬∃ (h' : 2 * k + 2 ≤ (↑(H.dropLast h).x).length), ((H.dropLast h).lift h').Lost) :

List.drop (2 * k + 1 + ⋯.num) ↑H.x ∈ ⋯.strat.pre.subtree