LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Strat

Auxiliary declarations for the Borel determinacy formalization.

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.Zero.takeLift y n = (GaleStewartGame.BorelDet.Zero.bodyTake y n).lift ⋯

@[simp]

theorem GaleStewartGame.BorelDet.Zero.takeLift_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) : ↑(takeLift y n).x = Stream'.take (2 * k + 2 + n) ↑y

@[simp]

theorem GaleStewartGame.BorelDet.Zero.takeLift_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) : (takeLift y n).R = (strategyEquivSystem R).str (2 * k)

@[simp]

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

@[simp]

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

theorem GaleStewartGame.BorelDet.Zero.losable_of_losable_not_lost {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) (hL : (takeLift y n).Losable) (h' : ∀ (m : ℕ), ¬(takeLift y m).Lost) (m : ℕ) (hm : ⋯.num ≤ m + 1) : (takeLift y m).Losable

theorem GaleStewartGame.BorelDet.Zero.body_lost_of_losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) (h : (takeLift y n).Losable) (h' : ∀ (m : ℕ), ¬(takeLift y m).Lost) : ⟨↑y, ⋯⟩ ∉ G.payoff

theorem GaleStewartGame.BorelDet.Zero.lost_of_body_lost {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (hy : ⟨↑y, ⋯⟩ ∉ G.payoff) : ∃ (m : ℕ), (takeLift y m).Lost

theorem GaleStewartGame.BorelDet.Zero.lost_of_losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (n : ℕ) (h : (takeLift y n).Losable) : ∃ (m : ℕ), (takeLift y m).Lost

noncomputable def GaleStewartGame.BorelDet.Zero.wonLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : ∀ (n : ℕ), (takeLift y n).Winnable) : ↑(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.Zero.wonLift_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : ∀ (n : ℕ), (takeLift y n).Winnable) : ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map π)) ⟨↑(wonLift y h), ⋯⟩) = ↑y

noncomputable def GaleStewartGame.BorelDet.Zero.lostLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : (takeLift y n).Lost) : ↑(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.Zero.lostLift_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} {R : Strategy (gameAsTrees hyp).snd Player.zero} (y : ↑(Descriptive.Tree.body (stratMap' R).pre.subtree)) (h : (takeLift y n).Lost) : ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map π)) ⟨↑(lostLift y h), ⋯⟩) = ↑y

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