LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Lift #

Auxiliary declarations for the Borel determinacy formalization.

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

QuasiStrategy (Descriptive.Tree.subAt H.game.tree [H.liftNode]) Player.one

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.liftShortWinStrat = (H.game.residual [H.liftNode]).defensiveQuasi GaleStewartGame.Player.one ⋯

Instances For

source

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

WLLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.toWLift = { toLift := H, liftTree := H.liftShortWinStrat.fst.subtree }

Instances For

source

@[simp]

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

H.toWLift.toLift = H

source

@[simp]

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

(H.take n h).toWLift.liftTree = H.toWLift.liftTree

source

@[simp]

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

(H.take n h).toWLift.liftMediumVal = H.toWLift.liftMediumVal

source

@[simp]

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

(H.take n h).toWLift.liftVal = List.take n H.toWLift.liftVal

source

theorem GaleStewartGame.BorelDet.Zero.Lift.wLift_liftVal_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H ≤ H') :

H.toWLift.liftVal <+: H'.toWLift.liftVal

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Winnable.take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hW : H.Winnable) (n : ℕ) (h : 2 * k + 2 ≤ n) :

(H.take n h).Winnable

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Winnable.liftMedium_mem {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hW : H.Winnable) :

H.toWLift.liftMediumVal ∈ T'

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.Winnable.toWLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hW : H.Winnable) :

WLLift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

hW.toWLift' = { toWLLift := H.toWLift, hlift := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Winnable.toWLift'_toWLLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hW : H.Winnable) :

hW.toWLift'.toWLLift = H.toWLift

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Winnable.extension_conLong {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hW : H.Winnable) (hp : IsPosition (↑hW.toWLift'.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑hW.toWLift'.x).length) :

(hW.toWLift'.extensionLift hp R).ConLong

source

structure GaleStewartGame.BorelDet.Zero.Lift.LLift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.Zero.Lift hyp :

Type u_1

Auxiliary declaration for the Borel determinacy formalization.

x : ↥G.tree
hlvl : 2 * k < (↑self.x).length
R : ResStrategy (gameAsTrees hyp) Player.zero (2 * k)
h'lvl : 2 * k + 1 < (↑self.x).length
conShort : self.ConShort
lost' : self.Lost'

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.Lift.LLift.ext {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : LLift hyp} (toLift : x.toLift = y.toLift) :

x = y

source

theorem GaleStewartGame.BorelDet.Zero.Lift.LLift.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : LLift hyp} :

x = y ↔ x.toLift = y.toLift

source

theorem GaleStewartGame.BorelDet.Zero.Lift.LLift.losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) (h : H.ConLong) :

H.Losable

source

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

∃ (n : ℕ) (h : 2 * k + 2 ≤ n), (H.take n h).Lost'

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.LLift.minLength {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

ℕ

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.minLength = Nat.find ⋯

Instances For

source

@[simp]

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

H.minLength ≤ (↑H.x).length

source

@[simp]

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

2 * k + 2 ≤ H.minLength

source

@[simp]

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

2 * k + 1 < H.minLength

Auxiliary declaration for the Borel determinacy formalization.

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.LLift.takeMin {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.takeMin = H.take H.minLength ⋯

Instances For

source

@[simp]

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

↑H.takeMin.x = List.take H.minLength ↑H.x

source

@[simp]

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

H.takeMin.R = H.R

source

@[simp]

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

H.takeMin.liftShort = H.liftShort

source

@[simp]

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

H.takeMin.game = H.game

source

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

H.takeMin.Lost'

source

theorem GaleStewartGame.BorelDet.Zero.Lift.LLift.le_of_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) {n : ℕ} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

H.minLength ≤ n

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.LLift.toWLLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

WLLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.toWLLift = { toLift := H.toLift, liftTree := Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree ↑H.takeMin.x) (List.drop (2 * k + 2) ↑H.takeMin.x) }

Instances For

source

@[simp]

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

H.toWLLift.toLift = H.toLift

source

def GaleStewartGame.BorelDet.Zero.Lift.Lost'.mk {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Lost') :

LLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.mk = { toLift := H, lost' := h }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost'.mk_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Lost') :

h.mk.toLift = H

source

def GaleStewartGame.BorelDet.Zero.Lift.extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

LLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.Zero.Lift.extend' hL = { toLift := H, lost' := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.extend'_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).toLift = H

source

theorem GaleStewartGame.BorelDet.Zero.Lift.extend'_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).minLength ≤ n

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.minLength_extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).minLength = hL.mk.minLength

source

theorem GaleStewartGame.BorelDet.Zero.Lift.extend'_le' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

hL.mk.minLength ≤ n

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.takeMin_extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).takeMin = hL.mk.takeMin

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.liftTree_extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).toWLLift.liftTree = hL.mk.toWLLift.liftTree

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.liftMediumVal_extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

(extend' hL).toWLLift.liftMediumVal = hL.mk.toWLLift.liftMediumVal

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.liftVal_extend' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost') :

List.take n (extend' hL).toWLLift.liftVal = hL.mk.toWLLift.liftVal

source

theorem GaleStewartGame.BorelDet.Zero.Lift.lost'_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H.Lost') (h' : H ≤ H') :

H'.Lost'

source

theorem GaleStewartGame.BorelDet.Zero.Lift.lLift_liftVal_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H.Lost') (h' : H ≤ H') :

h.mk.toWLLift.liftVal <+: ⋯.mk.toWLLift.liftVal

source

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

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.Lost = ∃ (h : H.Lost'), h.mk.takeMin.ConLong

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost.extend {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Lost) :

H.Lost

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost.lost_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H.Lost) (h' : H ≤ H') :

H'.Lost

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost.liftMedium_mem {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hL : H.Lost) :

⋯.mk.toWLLift.liftMediumVal ∈ T'

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost.lift_mem {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hL : H.Lost) (n : ℕ) :

(⋯.mk.toWLLift.liftMediumVal ++ (List.take n (List.drop (2 * k + 2) ↑H.x)).zipInitsMap fun (a : A) (y : List A) => (a, Descriptive.Tree.subAt ⋯.mk.toWLLift.liftTree y)) ∈ T'

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.Lost.toLLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hL : H.Lost) :

WLLift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

hL.toLLift' = { toWLLift := ⋯.mk.toWLLift, hlift := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Lost.toLLift'_toWLLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (hL : H.Lost) :

hL.toLLift'.toWLLift = ⋯.mk.toWLLift

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extend {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} {h : 2 * k + 2 ≤ n} (hL : (H.take n h).Losable) (hc : H.ConLong) :

H.Losable

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.losable_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H.Losable) (h' : H ≤ H') (hc : H'.ConLong) :

H'.Losable

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {H : Lift hyp} (h : H.Losable) (hn : 1 ≤ ⋯.num + n) :

(H.take (2 * k + 1 + ⋯.num + n) ⋯).Losable

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.Losable.x' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) :

↥(H.game.residual (List.take ⋯.num (List.drop (2 * k + 1) ↑H.x))).tree

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.x' = ⟨List.drop (2 * k + 1 + ⋯.num) ↑H.x, ⋯⟩

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.x'_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) :

↑h.x' = List.drop (2 * k + 1 + ⋯.num) ↑H.x

source

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

Descriptive.Tree.ExtensionsAt h.x'

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.a hp = ⋯.strat h.x' ⋯

Instances For

source

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

Descriptive.Tree.ExtensionsAt H.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.extension hp = ⟨↑(h.a hp), ⋯⟩

Instances For

source

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

PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.extensionPreLift hp = { x := (h.extension hp).valT', hlvl := ⋯, R := H.R }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionPreLift_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionPreLift hp).R = H.R

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionPreLift_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionPreLift hp).x = (h.extension hp).valT'

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionPreLift_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionPreLift hp).take (↑H.x).length ⋯ = H.toPreLift

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionPreLift_game {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionPreLift hp).game = H.game

source

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

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.extensionLift hp = { toPreLift := h.extensionPreLift hp, h'lvl := ⋯, conShort := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionLift_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionLift hp).toPreLift = h.extensionPreLift hp

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extensionLift_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionLift hp).take (↑H.x).length ⋯ = H

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Losable.extension_losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : Lift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.zero) :

(h.extensionLift hp).Losable

source

noncomputable def GaleStewartGame.BorelDet.Zero.Lift.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy ⟨upA hyp, T'⟩ Player.zero (↑H.x).length) :

Descriptive.Tree.ExtensionsAt H.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.Lift.extension_winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy ⟨upA hyp, T'⟩ Player.zero (↑H.x).length) (h : H.Winnable) :

H.extension hp R = h.toWLift'.extensionMap hp R