LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.BuildStrategies

Auxiliary declarations for the Borel determinacy formalization.

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

try following PreStrategy planA if possible, else follow planB

Equations

• planA.tryAndElse planB x hp = if (planA x hp).Nonempty then planA x hp else planB x hp

theorem GaleStewartGame.PreStrategy.tryAndElse_mono {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {planA planB planB' : PreStrategy T p} (hB : planB ≤ planB') : planA.tryAndElse planB ≤ planA.tryAndElse planB'

theorem GaleStewartGame.PreStrategy.quasi_of_planB {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {planA planB : PreStrategy T p} (h : planB.IsQuasi) : (planA.tryAndElse planB).IsQuasi

theorem GaleStewartGame.PreStrategy.planA_sub {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {planA planB : PreStrategy T p} : planA ≤ planA.tryAndElse planB

theorem GaleStewartGame.PreStrategy.eq_planA {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {planA planB : PreStrategy T p} (hQ : ∀ (x : ↥planA.subtree) (hp : IsPosition (↑x) p), ∃ (a : Descriptive.Tree.ExtensionsAt ⟨↑x, ⋯⟩), a ∈ planA ⟨↑x, ⋯⟩ hp) : (planA.tryAndElse planB).subtree = planA.subtree

@[simp]

theorem GaleStewartGame.PreStrategy.tryAndElse_residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {planA planB : PreStrategy T p} (x : List A) : (planA.tryAndElse planB).residual x = (planA.residual x).tryAndElse (planB.residual x)

@[implicit_reducible]

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

Equations

• GaleStewartGame.PreStrategy.instOrderBot T p = { bot := fun (x : ↥T) (x_1 : GaleStewartGame.IsPosition (↑x) p) => ∅, bot_le := ⋯ }

@[simp]

theorem GaleStewartGame.PreStrategy.eval_bot {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (x : ↥T) (hp : IsPosition (↑x) p) : ⊥ x hp = ∅

@[implicit_reducible]

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

Equations

• GaleStewartGame.PreStrategy.instOrderTop T p = { top := fun (x : ↥T) (x_1 : GaleStewartGame.IsPosition (↑x) p) => Set.univ, le_top := ⋯ }

@[simp]

theorem GaleStewartGame.PreStrategy.eval_top {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (x : ↥T) (hp : IsPosition (↑x) p) : ⊤ x hp = Set.univ

theorem GaleStewartGame.PreStrategy.top_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (h : Descriptive.Tree.IsPruned T) : ⊤.IsQuasi

@[simp]

theorem GaleStewartGame.PreStrategy.top_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} : ⊤.subtree = T

@[simp]

theorem GaleStewartGame.PreStrategy.top_residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (x : List A) : ⊤.residual x = ⊤

def GaleStewartGame.PreStrategy.emptyStrategy (A : Type u_1) (p : Player) : Strategy ⊥ p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.PreStrategy.emptyStrategy A p x x✝ = False.elim ⋯

@[simp]

theorem GaleStewartGame.PreStrategy.emptyStrategy_subtree {A : Type u_1} {p : Player} : (emptyStrategy A p).pre.subtree = ⊥

theorem GaleStewartGame.PreStrategy.existsWinning_empty {A : Type u_1} {p : Player} : { tree := ⊥, payoff := ∅ }.ExistsWinning p

theorem GaleStewartGame.Game.AllWinning.existsWinning {A : Type u_1} {p : Player} {G : Game A} (h : G.AllWinning p) (hP : Descriptive.Tree.IsPruned G.tree) : G.ExistsWinning p

@[reducible, inline]

abbrev GaleStewartGame.PreStrategy.extQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (h : Descriptive.Tree.IsPruned T) : QuasiStrategy T p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.extQuasi h = ⟨S.tryAndElse ⊤, ⋯⟩

theorem GaleStewartGame.PreStrategy.eq_extQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (hT : Descriptive.Tree.IsPruned T) (h : ∀ (x : ↥S.subtree) (hp : IsPosition (↑x) p), ∃ (a : Descriptive.Tree.ExtensionsAt (S.subtreeIncl x)), a ∈ S (S.subtreeIncl x) hp) : (S.extQuasi hT).fst.subtree = S.subtree

@[simp]

theorem GaleStewartGame.PreStrategy.extQuasi_residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (S : PreStrategy T p) (h : Descriptive.Tree.IsPruned T) (x : List A) : (S.extQuasi h).residual x = (S.residual x).extQuasi ⋯

def GaleStewartGame.PreStrategy.sew {A : Type u_1} {T : ↥(Descriptive.tree A)} (f : (a : A) → [a] ∈ T → PreStrategy (Descriptive.Tree.subAt T [a]) Player.zero) : PreStrategy T Player.one

sew a map from possible opponent moves to strategies in the resulting residual games to a strategy in the original game

Equations

• GaleStewartGame.PreStrategy.sew f ⟨[], property⟩ hp = ⋯.elim
• GaleStewartGame.PreStrategy.sew f ⟨a :: x_2, hx⟩ hp = f a ⋯ ⟨x_2, hx⟩ ⋯

theorem GaleStewartGame.PreStrategy.sew_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} (f : (a : A) → [a] ∈ T → PreStrategy (Descriptive.Tree.subAt T [a]) Player.zero) (hf : ∀ (a : A) (ha : [a] ∈ T), (f a ha).IsQuasi) : (sew f).IsQuasi

theorem GaleStewartGame.PreStrategy.sew_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} (f : (a : A) → [a] ∈ T → PreStrategy (Descriptive.Tree.subAt T [a]) Player.zero) (a : A) (x : List A) : a :: x ∈ (sew f).subtree ↔ ∃ (h : [a] ∈ T), x ∈ (f a h).subtree

theorem GaleStewartGame.PreStrategy.sew_body {A : Type u_1} {T : ↥(Descriptive.tree A)} (f : (a : A) → [a] ∈ T → PreStrategy (Descriptive.Tree.subAt T [a]) Player.zero) (x : Stream' A) (a : A) : Stream'.cons a x ∈ Descriptive.Tree.body (sew f).subtree ↔ ∃ (h : [a] ∈ T), x ∈ Descriptive.Tree.body (f a h).subtree

theorem GaleStewartGame.PreStrategy.sew_isWinning {A : Type u_1} {G : Game A} (f : (a : A) → [a] ∈ G.tree → PreStrategy (G.residual [a]).tree Player.zero) (h : ∀ (a : A) (h : [a] ∈ G.tree), (f a h).IsWinning) : (sew f).IsWinning

theorem GaleStewartGame.PreStrategy.sew_residual {A : Type u_1} {T : ↥(Descriptive.tree A)} (S : PreStrategy T Player.one) : (sew fun (a : A) (x : [a] ∈ T) => S.residual [a]) = S

noncomputable def GaleStewartGame.PreStrategy.firstMove {A : Type u_1} {T : ↥(Descriptive.tree A)} (a : A) (h : [a] ∈ T) (s : PreStrategy (Descriptive.Tree.subAt T [a]) Player.one) : PreStrategy T Player.zero

in the first move, play a, then follow s

Equations

• One or more equations did not get rendered due to their size.
• GaleStewartGame.PreStrategy.firstMove a h s ⟨[], property⟩ x_2 = {⟨a, h⟩}

@[simp]

theorem GaleStewartGame.PreStrategy.firstMove_subtree {A : Type u_1} {T : ↥(Descriptive.tree A)} (a : A) (h : [a] ∈ T) (s : PreStrategy (Descriptive.Tree.subAt T [a]) Player.one) (a' : A) (x : List A) : a' :: x ∈ (firstMove a h s).subtree ↔ a = a' ∧ x ∈ s.subtree

@[simp]

theorem GaleStewartGame.PreStrategy.firstMove_body {A : Type u_1} {T : ↥(Descriptive.tree A)} (a : A) (h : [a] ∈ T) (s : PreStrategy (Descriptive.Tree.subAt T [a]) Player.one) (a' : A) (x : Stream' A) : Stream'.cons a' x ∈ Descriptive.Tree.body (firstMove a h s).subtree ↔ a = a' ∧ x ∈ Descriptive.Tree.body s.subtree

@[simp]

theorem GaleStewartGame.PreStrategy.firstMove_isWinning {A : Type u_1} (a : A) {G : Game A} (h : [a] ∈ G.tree) (s : PreStrategy (G.residual [a]).tree Player.one) : (firstMove a h s).IsWinning ↔ s.IsWinning

theorem GaleStewartGame.PreStrategy.firstMove_extQuasi_tree {A : Type u_1} (a : A) {G : Game A} (h : [a] ∈ G.tree) (s : PreStrategy (G.residual [a]).tree Player.one) (hs : s.IsQuasi) (hT : Descriptive.Tree.IsPruned G.tree) : ((firstMove a h s).extQuasi hT).fst.subtree = (firstMove a h s).subtree

@[simp]

theorem GaleStewartGame.PreStrategy.firstMove_extQuasi_isWinning {A : Type u_1} (a : A) {G : Game A} (h : [a] ∈ G.tree) (s : PreStrategy (G.residual [a]).tree Player.one) (hT : Descriptive.Tree.IsPruned G.tree) (hs : s.IsQuasi) : ((firstMove a h s).extQuasi hT).fst.IsWinning ↔ s.IsWinning

def GaleStewartGame.PreStrategy.preserveProp {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (P : (x : ↥T) → IsPosition (↑x) p.swap → Prop) : PreStrategy T p

play such that the proposition P x holds in every position x resulting from your move

Equations

• GaleStewartGame.PreStrategy.preserveProp P x hp = {a : Descriptive.Tree.ExtensionsAt x | P a.valT' ⋯}

theorem GaleStewartGame.PreStrategy.preserveProp_eq_extQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} (P : (x : ↥T) → IsPosition (↑x) p.swap → Prop) (h : ∀ (x : ↥T) (hp : IsPosition (↑x) p.swap), P x hp → ∀ (a : Descriptive.Tree.ExtensionsAt x), (preserveProp P a.valT' ⋯).Nonempty) (hT : Descriptive.Tree.IsPruned T) (hst0 : ∀ (hp : p = Player.zero), ∃ (a : A) (ha : [a] ∈ T), P ⟨[a], ha⟩ ⋯) (hst1 : ∀ (hp : p = Player.one) (hn : [] ∈ T), P ⟨[], hn⟩ ⋯) : ((preserveProp P).extQuasi hT).fst.subtree = (preserveProp P).subtree

def GaleStewartGame.Game.WinningPosition {A : Type u_1} (G : Game A) (x : List A) (p : Player := Player.zero) : Prop

a position is winning if there is a winning strategy in the residual game

Equations

• G.WinningPosition x p = (G.residual x).ExistsWinning p

@[simp]

theorem GaleStewartGame.Game.winningPosition_residual {A : Type u_1} {G : Game A} {p : Player} (x y : List A) : (G.residual x).WinningPosition y p ↔ G.WinningPosition (x ++ y) p

def GaleStewartGame.Game.WonPosition {A : Type u_1} (G : Game A) (x : List A) (p : Player := Player.zero) : Prop

a position is won if it cannot be lost by playing however

Equations

• G.WonPosition x p = (G.residual x).AllWinning p

@[simp]

theorem GaleStewartGame.Game.wonPosition_residual {A : Type u_1} {G : Game A} {p : Player} (x y : List A) : (G.residual x).WonPosition y p ↔ G.WonPosition (x ++ y) p

theorem GaleStewartGame.Game.WonPosition.extend {A : Type u_1} {G : Game A} {p : Player} {x : List A} (y : List A) (hW : G.WonPosition x p) : G.WonPosition (x ++ y) (Player.residual y p)

theorem GaleStewartGame.Game.wonPosition_iff_disjoint' {A : Type u_1} {G : Game A} {p : Player} {x : List A} : G.WonPosition x p ↔ Set.range (Descriptive.Tree.body.append x) ∩ (Player.residual x p.swap).payoff G = ∅

theorem GaleStewartGame.Game.wonPosition_iff_disjoint {A : Type u_1} {G : Game A} {p : Player} {x : List A} : G.WonPosition x p ↔ Stream'.Discrete.principalOpen x ∩ Subtype.val '' (Player.residual x p.swap).payoff G = ∅

def GaleStewartGame.Game.defensivePre {A : Type u_1} (G : Game A) (p : Player) : PreStrategy G.tree p

the defensive PreStrategy never moves into a winning position of the opponent

Equations

• G.defensivePre p = GaleStewartGame.PreStrategy.preserveProp fun (x : ↥G.tree) (x_1 : GaleStewartGame.IsPosition (↑x) p.swap) => ¬G.WinningPosition ↑x

@[simp]

theorem GaleStewartGame.Game.defensivePre_residual {A : Type u_1} {G : Game A} {p : Player} {x : List A} : (G.defensivePre p).residual x = (G.residual x).defensivePre (Player.residual x p)

theorem GaleStewartGame.Game.defensivePre_subtree {A : Type u_1} {G G' : Game A} {p p' : Player} {hG : G = G'} {hp : p = p'} : (G.defensivePre p).subtree = (G'.defensivePre p').subtree

def GaleStewartGame.Game.defensiveQuasi {A : Type u_1} (G : Game A) (p : Player) (h : Descriptive.Tree.IsPruned G.tree) : QuasiStrategy G.tree p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• G.defensiveQuasi p = (G.defensivePre p).extQuasi

theorem GaleStewartGame.Game.defensiveQuasi_subtree {A : Type u_1} {G G' : Game A} {p p' : Player} {hG : G = G'} {hp : p = p'} (h : Descriptive.Tree.IsPruned G.tree) : (G.defensiveQuasi p h).fst.subtree = (G'.defensiveQuasi p' ⋯).fst.subtree

theorem GaleStewartGame.PreStrategy.subtree_induction_body {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : Player} {f g : PreStrategy T p} {x : Stream' A} (h : x ∈ Descriptive.Tree.body f.subtree) (h' : ∀ (n : ℕ), Stream'.take n x ∈ g.subtree → ∀ (hp : IsPosition (↑(f.subtreeIncl (Descriptive.Tree.body.take n ⟨x, h⟩))) p), ⟨x.get n, ⋯⟩ ∈ f (f.subtreeIncl (Descriptive.Tree.body.take n ⟨x, h⟩)) hp → ⟨x.get n, ⋯⟩ ∈ g (f.subtreeIncl (Descriptive.Tree.body.take n ⟨x, h⟩)) hp) : x ∈ Descriptive.Tree.body g.subtree

noncomputable def GaleStewartGame.PreStrategy.followUntilWon {A : Type u_1} {G : Game A} {p : Player} (S : PreStrategy G.tree p) : PreStrategy G.tree p

Auxiliary declaration for the Borel determinacy formalization.

Equations

• S.followUntilWon x hp = if G.WonPosition (↑x) (GaleStewartGame.Player.residual (↑x) p) then Set.univ else S x hp

theorem GaleStewartGame.PreStrategy.le_followUntilWon {A : Type u_1} {G : Game A} {p : Player} (S : PreStrategy G.tree p) : S ≤ S.followUntilWon

theorem GaleStewartGame.PreStrategy.followUntilWon_body {A : Type u_1} {G : Game A} {p : Player} (S : PreStrategy G.tree p) : Descriptive.Tree.body S.followUntilWon.subtree ≤ Descriptive.Tree.body S.subtree ∪ Subtype.val '' p.payoff G

@[simp]

theorem GaleStewartGame.PreStrategy.followUntilWon_isWinning {A : Type u_1} {G : Game A} {p : Player} (S : PreStrategy G.tree p) : S.followUntilWon.IsWinning ↔ S.IsWinning