LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Strategies

Auxiliary declarations for the Borel determinacy formalization.

def GaleStewartGame.PreStrategy {A : Type u_1} (T : ↥(Descriptive.tree A)) (p : Player) : Type u_1

a PreStrategy is a weak form of a strategy given by specifying not a single move, but a possibly empty set of valid moves in all positions. This can be defined for arbitrary trees and not just games as the payoff set is irrelevant

Equations

• GaleStewartGame.PreStrategy T p = ((x : ↥T) → GaleStewartGame.IsPosition (↑x) p → Set (Descriptive.Tree.ExtensionsAt x))

theorem GaleStewartGame.PreStrategy.ext {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : PreStrategy T p} (h : ∀ (x : ↥T) (hp : IsPosition (↑x) p), f x hp = g x hp) : f = g

theorem GaleStewartGame.PreStrategy.ext_iff {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : PreStrategy T p} : f = g ↔ ∀ (x : ↥T) (hp : IsPosition (↑x) p), f x hp = g x hp

@[implicit_reducible]

instance GaleStewartGame.PreStrategy.instPartialOrder {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} : PartialOrder (PreStrategy T p)

Equations

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

def GaleStewartGame.PreStrategy.subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) : ↥(Descriptive.tree A)

the tree of plays valid with a PreStrategy

Equations

• S.subtree = ⟨{x : List A | ∃ (hx : x ∈ T), ∀ {y : List A} {a : A} (hpr : y ++ [a] <+: x) (hpo : GaleStewartGame.IsPosition y p), ⟨a, ⋯⟩ ∈ S ⟨y, ⋯⟩ hpo}, ⋯⟩

@[simp]

theorem GaleStewartGame.PreStrategy.subtree_ne {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) : [] ∈ S.subtree ↔ [] ∈ T

Auxiliary declaration for the Borel determinacy formalization.

@[simp]

theorem GaleStewartGame.PreStrategy.subtree_sub {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) : S.subtree ≤ T

def GaleStewartGame.PreStrategy.subtreeIncl {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) : ↥T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.subtreeIncl x = ⟨↑x, ⋯⟩

@[simp]

theorem GaleStewartGame.PreStrategy.subtreeIncl_coe {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) : ↑(S.subtreeIncl x) = ↑x

theorem GaleStewartGame.PreStrategy.subtree_mono {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : PreStrategy T p} (h : f ≤ g) : f.subtree ≤ g.subtree

theorem GaleStewartGame.PreStrategy.subtree_fair {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) {a : A} (hp : IsPosition (↑x) p.swap) : ↑x ++ [a] ∈ S.subtree ↔ ↑x ++ [a] ∈ T

theorem GaleStewartGame.PreStrategy.subtree_compatible {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) (hp : IsPosition (↑x) p) {a : A} (hx : ↑x ++ [a] ∈ S.subtree) : ⟨a, ⋯⟩ ∈ S (S.subtreeIncl x) hp

theorem GaleStewartGame.PreStrategy.subtree_compatible_iff {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) (hp : IsPosition (↑x) p) {a : A} : ↑x ++ [a] ∈ S.subtree ↔ ∃ (hx : ↑x ++ [a] ∈ T), ⟨a, hx⟩ ∈ S (S.subtreeIncl x) hp

theorem GaleStewartGame.PreStrategy.subtree_induction {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {S S' : PreStrategy T p} {x : List A} (h : x ∈ S.subtree) (h' : ∀ (n : ℕ) (hn : n < x.length), List.take n x ∈ S'.subtree → ∀ (hp : IsPosition (↑(Descriptive.Tree.take n (S.subtreeIncl ⟨x, h⟩))) p), ⟨x[n], ⋯⟩ ∈ S (Descriptive.Tree.take n (S.subtreeIncl ⟨x, h⟩)) hp → ⟨x[n], ⋯⟩ ∈ S' (Descriptive.Tree.take n (S.subtreeIncl ⟨x, h⟩)) hp) : x ∈ S'.subtree

def GaleStewartGame.PreStrategy.restrictTree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (rto : ↥(Descriptive.tree A)) (hr : rto ≤ T) : PreStrategy rto p

restrict a PreStrategy to a subtree of the game tree

Equations

• S.restrictTree rto hr x hx a = S ⟨↑x, ⋯⟩ hx ⟨↑a, ⋯⟩

@[reducible, inline]

abbrev GaleStewartGame.PreStrategy.restrict {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (rto : PreStrategy T p.swap) : PreStrategy rto.subtree p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.restrict rto = S.restrictTree rto.subtree ⋯

theorem GaleStewartGame.PreStrategy.restrict_sub {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (rto : ↥(Descriptive.tree A)) (hr : rto ≤ T) : (S.restrictTree rto hr).subtree ≤ S.subtree

theorem GaleStewartGame.PreStrategy.restrict_valid {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (rto : ↥(Descriptive.tree A)) (hr : rto ≤ T) : (S.restrictTree rto hr).subtree ≤ rto

@[simp]

theorem GaleStewartGame.PreStrategy.restrict_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (rto : ↥(Descriptive.tree A)) (hr : rto ≤ T) : (S.restrictTree rto hr).subtree = S.subtree ⊓ rto

def GaleStewartGame.PreStrategy.residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : List A) : PreStrategy (Descriptive.Tree.subAt T x) (Player.residual x p)

the residual strategy for the game starting in position x

Equations

• S.residual x y hy = {a : Descriptive.Tree.ExtensionsAt y | ⟨↑a, ⋯⟩ ∈ S ⟨x ++ ↑y, ⋯⟩ ⋯}

theorem GaleStewartGame.PreStrategy.sub_residual_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : List A) : Descriptive.Tree.subAt S.subtree x ≤ (S.residual x).subtree

@[simp]

theorem GaleStewartGame.PreStrategy.residual_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (x : ↥S.subtree) : (S.residual ↑x).subtree = Descriptive.Tree.subAt S.subtree ↑x

def GaleStewartGame.PreStrategy.IsQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) : Prop

A quasistrategy is a PreStrategy that allows at least one move in every position

Equations

• S.IsQuasi = ∀ (x : ↥T) (hx : GaleStewartGame.IsPosition (↑x) p), (S x hx).Nonempty

def GaleStewartGame.QuasiStrategy {A : Type u_1} (T : ↥(Descriptive.tree A)) (p : Player) : Type u_1

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.QuasiStrategy T p = PSigma GaleStewartGame.PreStrategy.IsQuasi

theorem GaleStewartGame.QuasiStrategy.ext {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : QuasiStrategy T p} (h : f.fst = g.fst) : f = g

theorem GaleStewartGame.QuasiStrategy.ext_iff {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : QuasiStrategy T p} : f = g ↔ f.fst = g.fst

def GaleStewartGame.Strategy {A : Type u_1} (T : ↥(Descriptive.tree A)) (p : Player) : Type u_1

A quasistrategy is a PreStrategy that allows exactly one move in every position

Equations

• GaleStewartGame.Strategy T p = ((x : ↥T) → GaleStewartGame.IsPosition (↑x) p → Descriptive.Tree.ExtensionsAt x)

theorem GaleStewartGame.Strategy.ext {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : Strategy T p} (h : ∀ (x : ↥T) (hp : IsPosition (↑x) p), f x hp = g x hp) : f = g

theorem GaleStewartGame.Strategy.ext_iff {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : Strategy T p} : f = g ↔ ∀ (x : ↥T) (hp : IsPosition (↑x) p), f x hp = g x hp

theorem GaleStewartGame.PreStrategy.eval_val_congr {A : Type u_1} {p : Player} {U : ↥(Descriptive.tree A)} (S S' : PreStrategy U p) (h : S = S') (x x' : ↥U) (h' : x = x') (hp : IsPosition (↑x) p) : Subtype.val '' S x hp = Subtype.val '' S' x' ⋯

theorem GaleStewartGame.PreStrategy.eval_mem_congr {A : Type u_1} {p : Player} {U : ↥(Descriptive.tree A)} (S : PreStrategy U p) {x x' : ↥U} (hx : x = x') (hp : IsPosition (↑x) p) (hp' : IsPosition (↑x') p) {a : Descriptive.Tree.ExtensionsAt x} {a' : Descriptive.Tree.ExtensionsAt x'} (ha : ↑a = ↑a') : a ∈ S x hp ↔ a' ∈ S x' hp'

theorem GaleStewartGame.Strategy.eval_val_congr {A : Type u_1} {p : Player} {U : ↥(Descriptive.tree A)} (S S' : Strategy U p) (h : S = S') (x x' : ↥U) (h' : x = x') (hp : IsPosition (↑x) p) : ↑(S x hp) = ↑(S' x' ⋯)

@[reducible, inline]

abbrev GaleStewartGame.Strategy.pre {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : Strategy T p) : PreStrategy T p

regard a Strategy as PreStrategy

Equations

• S.pre x hx = {S x hx}

@[simp]

theorem GaleStewartGame.Strategy.isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : Strategy T p) : S.pre.IsQuasi

@[reducible, inline]

abbrev GaleStewartGame.Strategy.quasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : Strategy T p) : QuasiStrategy T p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.quasi = ⟨S.pre, ⋯⟩

noncomputable def GaleStewartGame.PreStrategy.IsQuasi.choose {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {S : PreStrategy T p} (h : S.IsQuasi) : Strategy T p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• h.choose x hp = ⋯.some

theorem GaleStewartGame.PreStrategy.choose_sub {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {S : PreStrategy T p} (h : S.IsQuasi) : h.choose.pre ≤ S

theorem GaleStewartGame.QuasiStrategy.subtree_isPruned {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : QuasiStrategy T p) (hT : Descriptive.Tree.IsPruned T) : Descriptive.Tree.IsPruned S.fst.subtree

theorem GaleStewartGame.PreStrategy.IsQuasi.restrictTree_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {S : PreStrategy T p} (rto : ↥(Descriptive.tree A)) (h : S.IsQuasi) (hfair : ∀ (x : ↥rto) (a : A), IsPosition (↑x) p → ↑x ++ [a] ∈ T → ↑x ++ [a] ∈ rto) (hr : rto ≤ T) : (S.restrictTree rto hr).IsQuasi

theorem GaleStewartGame.PreStrategy.IsQuasi.restrict_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {S : PreStrategy T p} (rto : PreStrategy T p.swap) (h : S.IsQuasi) : (S.restrict rto).IsQuasi

@[reducible, inline]

abbrev GaleStewartGame.QuasiStrategy.restrict {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : QuasiStrategy T p) (rto : PreStrategy T p.swap) : QuasiStrategy rto.subtree p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.restrict rto = ⟨S.fst.restrict rto, ⋯⟩

def GaleStewartGame.QuasiStrategy.residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : QuasiStrategy T p) (x : List A) : QuasiStrategy (Descriptive.Tree.subAt T x) (Player.residual x p)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.residual x = ⟨S.fst.residual x, ⋯⟩

@[simp]

theorem GaleStewartGame.QuasiStrategy.residual_fst {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : QuasiStrategy T p) (x : List A) : (S.residual x).fst = S.fst.residual x