LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Undetermined

Auxiliary declarations for the Borel determinacy formalization.

def GaleStewartGame.Player.ownTree {A : Type u_1} (p : Player) (a : Stream' A) : Strategy ⊤ p

the strategy which plays the infinite sequence a independent of the opponents' moves

Equations

• p.ownTree a x x✝ = ⟨a.get ((↑x).length / 2), ⋯⟩

@[simp]

theorem GaleStewartGame.Player.ownTree.mem_body {A : Type u_1} {p : Player} {a x : Stream' A} : x ∈ Descriptive.Tree.body (p.ownTree a).pre.subtree ↔ ∀ (n : ℕ), x.get (2 * n + p.toNat) = a.get n

theorem GaleStewartGame.Player.ownTree.disjoint {A : Type u_1} {p : Player} {a b : Stream' A} (h : a ≠ b) : Descriptive.Tree.body (p.ownTree a).pre.subtree ∩ Descriptive.Tree.body (p.ownTree b).pre.subtree = ∅

theorem GaleStewartGame.QuasiStrategy.subtree_top_large {A : Type u_1} {p : Player} (h : 2 ≤ Cardinal.mk A) (S : QuasiStrategy ⊤ p) : Cardinal.continuum ≤ Cardinal.mk ↑(Descriptive.Tree.body S.fst.subtree)

@[simp]

theorem GaleStewartGame.card_player : Cardinal.mk Player = 2

theorem GaleStewartGame.Game.exists_undetermined : ∃ (G : Game (Fin 2)), Descriptive.Tree.IsPruned G.tree ∧ [] ∈ G.tree ∧ ¬G.IsDetermined