LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringClosedGame #

Auxiliary declarations for the Borel determinacy formalization.

source

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

Prop

Auxiliary declaration for the Borel determinacy formalization.

closed : IsClosed G.payoff
pruned : Descriptive.Tree.IsPruned G.tree
nonempty : [] ∈ G.tree

Instances For

source

def GaleStewartGame.BorelDet.upA {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

Type u_1

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.upA hyp = (A × ↥(Descriptive.tree A))

Instances For

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.A' {A : Type u_2} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

Type u_2

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.A' = GaleStewartGame.BorelDet.upA hyp

Instances For

source

def GaleStewartGame.BorelDet.getTree' {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) (x : List (upA hyp)) :

↥(Descriptive.tree A)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.getTree' hyp x = match x.getLast? with | none => G.tree | some a => a.2

Instances For

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.getTree {A : Type u_2} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List A') :

↥(Descriptive.tree A)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.getTree x = GaleStewartGame.BorelDet.getTree' hyp x

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.getTree_nil {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

getTree' hyp [] = G.tree

source

@[simp]

theorem GaleStewartGame.BorelDet.getTree_concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (a : upA hyp) :

getTree' hyp (x ++ [a]) = a.2

source

def GaleStewartGame.BorelDet.LosingCondition {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (h : x.length = 2 * k + 2) :

Prop

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.LosingCondition.concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} {h : (x ++ [a]).length = 2 * k + 2} :

LosingCondition (x ++ [a]) h ↔ Descriptive.Tree.body (Descriptive.Tree.pullSub a.2 (List.map Prod.fst x ++ [a.1])) ∩ Subtype.val '' G.payoff = ∅ ∧ ∃ (y : ↥(Descriptive.Tree.subAt (getTree' hyp x) [a.1])), a.2 = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.map Prod.fst x ++ a.1 :: ↑y)) ↑y

source

theorem GaleStewartGame.BorelDet.LosingCondition.of_concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} {h : (x ++ [a]).length = 2 * k + 2} (H : LosingCondition (x ++ [a]) h) :

∃ (y : ↥(Descriptive.Tree.subAt (getTree' hyp x) [a.1])), a.2 = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.map Prod.fst x ++ a.1 :: ↑y)) ↑y

source

def GaleStewartGame.BorelDet.WinningCondition {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (h : x.length = 2 * k + 2) :

Prop

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.cast_subtree {A : Type u_2} {T T' : ↥(Descriptive.tree A)} {p p' : Player} (hT : T = T') (hp : p = p') (S : QuasiStrategy T p) :

(cast ⋯ S).fst.subtree = S.fst.subtree

source

theorem GaleStewartGame.BorelDet.WinningCondition.concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} {h : (x ++ [a]).length = 2 * k + 2} :

WinningCondition (x ++ [a]) h ↔ Descriptive.Tree.body (Descriptive.Tree.pullSub a.2 (List.map Prod.fst x ++ [a.1])) ⊆ Subtype.val '' G.payoff ∧ ∃ (S' : QuasiStrategy (Descriptive.Tree.subAt (getTree' hyp x) [a.1]) Player.one), a.2 = S'.fst.subtree

source

theorem GaleStewartGame.BorelDet.WinningCondition.of_concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} {h : (x ++ [a]).length = 2 * k + 2} (H : WinningCondition (x ++ [a]) h) :

∃ (S' : QuasiStrategy (Descriptive.Tree.subAt (getTree' hyp x) [a.1]) Player.one), a.2 = S'.fst.subtree

source

def GaleStewartGame.BorelDet.ValidExt {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (a : upA hyp) :

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.validExt_zero {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} (h : x.length = 2 * k) :

ValidExt x a ↔ [a.1] ∈ getTree' hyp x ∧ ∃ (S : QuasiStrategy (Descriptive.Tree.subAt (getTree' hyp x) [a.1]) Player.one), a.2 = S.fst.subtree

source

@[simp]

theorem GaleStewartGame.BorelDet.validExt_one {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} (h : x.length = 2 * k + 1) :

ValidExt x a ↔ [a.1] ∈ getTree' hyp x ∧ (LosingCondition (x ++ [a]) ⋯ ∨ WinningCondition (x ++ [a]) ⋯)

source

@[simp]

theorem GaleStewartGame.BorelDet.validExt_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} (h : x.length < 2 * k) :

ValidExt x a ↔ [a.1] ∈ getTree' hyp x ∧ a.2 = Descriptive.Tree.subAt (getTree' hyp x) [a.1]

source

@[simp]

theorem GaleStewartGame.BorelDet.validExt_long {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} (h : 2 * k + 2 ≤ x.length) :

ValidExt x a ↔ [a.1] ∈ getTree' hyp x ∧ a.2 = Descriptive.Tree.subAt (getTree' hyp x) [a.1]

source

def GaleStewartGame.BorelDet.gameTree {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

↥(Descriptive.tree (upA hyp))

the tree of the unraveled game of a closed game

Equations

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

Instances For

source

def GaleStewartGame.BorelDet.oldAsTrees {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

Descriptive.Tree.Trees

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.oldAsTrees hyp = ⟨A, G.tree⟩

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.oldAsTrees_snd {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(oldAsTrees hyp).snd = G.tree

source

@[simp]

theorem GaleStewartGame.BorelDet.oldAsTrees_fst {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(oldAsTrees hyp).fst = A

source

def GaleStewartGame.BorelDet.gameAsTrees {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

Descriptive.Tree.Trees

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.gameAsTrees hyp = ⟨GaleStewartGame.BorelDet.upA hyp, GaleStewartGame.BorelDet.gameTree hyp⟩

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.gameAsTrees_fst {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(gameAsTrees hyp).fst = upA hyp

source

@[simp]

theorem GaleStewartGame.BorelDet.gameAsTrees_snd {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(gameAsTrees hyp).snd = gameTree hyp

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.T {A : Type u_2} {G : Game A} :

↥(Descriptive.tree A)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.T = G.tree

Instances For

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.T' {A : Type u_2} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

↥(Descriptive.tree (upA hyp))

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.T' = GaleStewartGame.BorelDet.gameTree hyp

Instances For

source

theorem GaleStewartGame.BorelDet.gameTree_ne {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

[] ∈ gameTree hyp

source

@[simp]

theorem GaleStewartGame.BorelDet.gameTree_concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (a : upA hyp) :

x ++ [a] ∈ gameTree hyp ↔ x ∈ gameTree hyp ∧ ValidExt x a

source

theorem GaleStewartGame.BorelDet.getTree_sub {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) :

getTree' hyp ↑x ≤ Descriptive.Tree.subAt G.tree (List.map Prod.fst ↑x)

source

theorem GaleStewartGame.BorelDet.getTree_ne_and_pruned {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) :

[] ∈ getTree' hyp ↑x ∧ Descriptive.Tree.IsPruned (getTree' hyp ↑x)

source

noncomputable def GaleStewartGame.BorelDet.LosingCondition.y {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} (H : LosingCondition (↑x) h) :

↥(getTree' hyp ↑x)

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.y = ⟨↑⋯.choose, ⋯⟩

Instances For

source

theorem GaleStewartGame.BorelDet.LosingCondition.y_spec {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} (H : LosingCondition (↑x) h) :

getTree' hyp ↑x = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.map Prod.fst ↑x ++ ↑H.y)) ↑H.y

source

noncomputable def GaleStewartGame.BorelDet.WinningCondition.S {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} (H : WinningCondition (↑x) h) :

QuasiStrategy (Descriptive.Tree.subAt (getTree' hyp (List.take (2 * k + 1) ↑x)) [(↑x)[2 * k + 1].1]) Player.one

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.S = ⋯.choose

Instances For

source

theorem GaleStewartGame.BorelDet.WinningCondition.S_spec {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} (H : WinningCondition (↑x) h) :

getTree' hyp ↑x = H.S.fst.subtree

source

theorem GaleStewartGame.BorelDet.lose_or_win {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) (h : (↑x).length = 2 * k + 2) :

LosingCondition (↑x) h ∨ WinningCondition (↑x) h

source

@[simp]

theorem GaleStewartGame.BorelDet.not_winning {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} :

¬WinningCondition (↑x) h ↔ LosingCondition (↑x) h

source

@[simp]

theorem GaleStewartGame.BorelDet.not_losing {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameTree hyp)} {h : (↑x).length = 2 * k + 2} :

¬LosingCondition (↑x) h ↔ WinningCondition (↑x) h

source

def GaleStewartGame.BorelDet.treeHom {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

gameAsTrees hyp ⟶ oldAsTrees hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.treeHom hyp = { toFun := fun (x : ↑↑(GaleStewartGame.BorelDet.gameAsTrees hyp).snd) => ⟨List.map Prod.fst ↑x, ⋯⟩, monotone' := ⋯, h_length := ⋯ }

Instances For

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.π {A : Type u_2} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

gameAsTrees hyp ⟶ oldAsTrees hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.π = GaleStewartGame.BorelDet.treeHom hyp

Instances For

source

def GaleStewartGame.BorelDet.pInvTreeHomMap {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) (x : List A) :

List (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.pInvTreeHomMap hyp x = x.zipInitsMap fun (a : A) (y : List A) => (a, (G.residual y).tree)

Instances For

source

theorem GaleStewartGame.BorelDet.treeHom_val {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) (gameAsTrees hyp)) :

↑((CategoryTheory.ConcreteCategory.hom (treeHom hyp)) x) = List.map Prod.fst ↑x

source

theorem GaleStewartGame.BorelDet.treeHom_body {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↑(Descriptive.Tree.body (gameTree hyp))) :

↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map (treeHom hyp))) x) = Stream'.map Prod.fst ↑x

source

theorem GaleStewartGame.BorelDet.T'_snd_small' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) (h : (↑x).length ≤ 2 * k) :

getTree' hyp ↑x = Descriptive.Tree.subAt G.tree (List.map Prod.fst ↑x)

source

theorem GaleStewartGame.BorelDet.T'_snd_small {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : List (upA hyp)} {a : upA hyp} (h : x ++ [a] ∈ gameTree hyp) (h' : x.length < 2 * k) :

a.2 = (G.residual (List.map Prod.fst x ++ [a.1])).tree

source

@[simp]

theorem GaleStewartGame.BorelDet.pInvTreeHomMap_nil {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

pInvTreeHomMap hyp [] = []

source

@[simp]

theorem GaleStewartGame.BorelDet.pInvTreeHomMap_concat {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List A) (a : A) :

pInvTreeHomMap hyp (x ++ [a]) = pInvTreeHomMap hyp x ++ [(a, (G.residual (x ++ [a])).tree)]

source

@[simp]

theorem GaleStewartGame.BorelDet.pInvTreeHomMap_len {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List A) :

(pInvTreeHomMap hyp x).length = x.length

source

@[simp]

theorem GaleStewartGame.BorelDet.getTree_pInvTreeHomMap {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List A) :

getTree' hyp (pInvTreeHomMap hyp x) = (G.residual x).tree

source

def GaleStewartGame.BorelDet.pInvTreeHom {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(Descriptive.Tree.res (2 * k)).obj ⟨A, G.tree⟩ ⟶ (Descriptive.Tree.res (2 * k)).obj ⟨upA hyp, gameTree hyp⟩

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.pInvTreeHom_val {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) (x : ↑↑((Descriptive.Tree.res (2 * k)).obj ⟨A, G.tree⟩).snd) :

↑((CategoryTheory.ConcreteCategory.hom (pInvTreeHom hyp)) x) = pInvTreeHomMap hyp ↑x

source

def GaleStewartGame.BorelDet.treeHomRes {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(Descriptive.Tree.res (2 * k)).obj ⟨upA hyp, gameTree hyp⟩ ≅ (Descriptive.Tree.res (2 * k)).obj ⟨A, G.tree⟩

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

instance GaleStewartGame.BorelDet.treeHom_fixing {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

Descriptive.Tree.Fixing (2 * k) (treeHom hyp)

source

@[simp]

theorem GaleStewartGame.BorelDet.pInv_treeHom_val {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) (x : ↑↑(oldAsTrees hyp).snd) (h : (↑x).length ≤ 2 * k) :

↑(Descriptive.Tree.pInv (treeHom hyp) x ⋯) = pInvTreeHomMap hyp ↑x

source

theorem GaleStewartGame.BorelDet.gameTree_isPruned {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

Descriptive.Tree.IsPruned (gameTree hyp)

source

def GaleStewartGame.BorelDet.game {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

Game (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.game_tree {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(game hyp).tree = gameTree hyp

source

@[simp]

theorem GaleStewartGame.BorelDet.game_payoff {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) :

(game hyp).payoff = ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map (treeHom hyp))) ⁻¹' G.payoff

source

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.G' {A : Type u_2} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

Game (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.BorelDet.G' = GaleStewartGame.BorelDet.game hyp

Instances For

source

theorem GaleStewartGame.BorelDet.getTree_eq' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : List (upA hyp)) (h : x ∈ gameTree hyp) :

getTree' hyp x = Descriptive.Tree.subAt (getTree' hyp (List.take (2 * k + 2) x)) (List.map Prod.fst (List.drop (2 * k + 2) x))

source

theorem GaleStewartGame.BorelDet.getTree_eq {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) :

getTree' hyp ↑x = Descriptive.Tree.subAt (getTree' hyp (List.take (2 * k + 2) ↑x)) (List.map Prod.fst (List.drop (2 * k + 2) ↑x))

source

theorem GaleStewartGame.BorelDet.mem_getTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) :

List.map Prod.fst ↑x ∈ Descriptive.Tree.pullSub (getTree' hyp (List.take (2 * k + 2) ↑x)) (List.map Prod.fst (List.take (2 * k + 2) ↑x))

source

theorem GaleStewartGame.BorelDet.wins_iff_answer {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↑(Descriptive.Tree.body (game hyp).tree)) :

x ∈ (game hyp).payoff ↔ WinningCondition (Stream'.take (2 * k + 2) ↑x) ⋯

source

@[implicit_reducible]

instance GaleStewartGame.BorelDet.instTopologicalSpaceUpA {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

TopologicalSpace (upA hyp)

Equations

GaleStewartGame.BorelDet.instTopologicalSpaceUpA = ⊥

source

instance GaleStewartGame.BorelDet.instDiscreteTopologyUpA {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

DiscreteTopology (upA hyp)

source

theorem GaleStewartGame.BorelDet.payoff_clopen {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

IsClopen (game hyp).payoff

source

theorem GaleStewartGame.BorelDet.T'_snd_medium' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (x : ↥(gameTree hyp)) (h : (↑x).length = 2 * k + 1) :

∃ (S : QuasiStrategy (G.residual (List.map Prod.fst ↑x)).tree Player.one), getTree' hyp ↑x = S.fst.subtree

source

@[simp]

theorem GaleStewartGame.BorelDet.treeHom_extensions_val {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(gameAsTrees hyp).snd} (a : Descriptive.Tree.ExtensionsAt x) {y : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) (oldAsTrees hyp)} (h : (CategoryTheory.ConcreteCategory.hom (treeHom hyp)) x = y) :

↑(Descriptive.Tree.ExtensionsAt.map (treeHom hyp) h a) = (↑a).1

source

theorem GaleStewartGame.BorelDet.extensionsAt_ext_fst {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(game hyp).tree} (a b : Descriptive.Tree.ExtensionsAt x) (hx : 2 * k + 2 ≤ (↑x).length) (h : (↑a).1 = (↑b).1) :

a = b

source

theorem GaleStewartGame.BorelDet.getTree_lost {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(game hyp).tree} (y : ↥(game hyp).tree) (h : ↑x <+: ↑y) (hxl : (↑x).length = 2 * k + 2) (hL : G.WonPosition (List.map Prod.fst ↑y) (Player.residual (↑y) Player.one)) :

LosingCondition (↑x) hxl

source

theorem GaleStewartGame.BorelDet.LosingCondition.not_lost_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(game hyp).tree} (hxl : 2 * k + 2 ≤ (↑x).length) (H : LosingCondition ↑(Descriptive.Tree.take (2 * k + 2) x) ⋯) (hnL : ¬G.WonPosition (List.map Prod.fst ↑x) (Player.residual (↑x) Player.one)) :

(↑x).length + 1 ≤ 2 * k + 2 + (↑H.y).length

source

theorem GaleStewartGame.BorelDet.extensionsAt_eq_of_lost {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x : ↥(game hyp).tree} (y : ↥(game hyp).tree) (h : ↑x <+: ↑y) (hxl : 2 * k + 2 ≤ (↑x).length) (hnL : ¬G.WonPosition (List.map Prod.fst ↑x) (Player.residual (↑x) Player.one)) (hL : G.WonPosition (List.map Prod.fst ↑y) (Player.residual (↑y) Player.one)) {a b : Descriptive.Tree.ExtensionsAt x} :

a = b