LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.WinAsap

Auxiliary declarations for the Borel determinacy formalization.

theorem choose_eq {α : Type u_1} {p q : α → Prop} (hpq : ∀ (a : α), p a ↔ q a) (h : ∃ (a : α), p a) : h.choose = ⋯.choose

theorem choose_eq' {α β : Type u} {p : α → Prop} {q : β → Prop} (hab : α = β) (hpq : ∀ (a : α), p a ↔ q (cast hab a)) (h : ∃ (a : α), p a) : h.choose ≍ ⋯.choose

def GaleStewartGame.PreStrategy.WinningPrefix {A : Type u_1} (G : Game A) (p : Player) (x : List A) : Prop

whether there exists a prefix of x that is a winning position for p

Equations

• GaleStewartGame.PreStrategy.WinningPrefix G p x = ∃ (n : ℕ), (G.residual (List.take n x)).ExistsWinning (GaleStewartGame.Player.residual (List.take n x) p)

theorem GaleStewartGame.PreStrategy.winningPrefix_of_notMem {A : Type u_1} (G : Game A) (p : Player) {x : List A} (h : x ∉ G.tree) : WinningPrefix G p x

theorem GaleStewartGame.Game.WinningPosition.winningPrefix {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : G.WinningPosition x p) : PreStrategy.WinningPrefix G (Player.residual x p) x

theorem GaleStewartGame.PreStrategy.WinningPrefix.mem_defensiveQuasi {A : Type u_1} {G : Game A} {p : Player} (x : ↥G.tree) (h : ¬WinningPrefix G p.swap ↑x) (hpr : Descriptive.Tree.IsPruned G.tree) : ↑x ∈ (G.defensiveQuasi p hpr).fst.subtree

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

noncomputable def GaleStewartGame.PreStrategy.WinningPrefix.num {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : ℕ

the length of the shortest prefix of x that is winning for p

Equations

• h.num = Nat.find h

theorem GaleStewartGame.PreStrategy.WinningPrefix.num_spec {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : (G.residual (List.take h.num x)).ExistsWinning (Player.residual (List.take h.num x) p)

@[simp]

theorem GaleStewartGame.PreStrategy.WinningPrefix.num_le_length {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : h.num ≤ x.length

theorem GaleStewartGame.PreStrategy.WinningPrefix.take_num {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} : List.take h.num (x ++ y) = List.take h.num x

theorem GaleStewartGame.PreStrategy.WinningPrefix.extend {A : Type u_1} {G : Game A} {p : Player} {x : List A} (y : List A) (h : WinningPrefix G p x) : WinningPrefix G p (x ++ y)

theorem GaleStewartGame.PreStrategy.WinningPrefix.of_take {A : Type u_1} {G : Game A} {p : Player} {x : List A} {n : ℕ} (h : WinningPrefix G p (List.take n x)) : WinningPrefix G p x

theorem GaleStewartGame.PreStrategy.WinningPrefix.of_prefix {A : Type u_1} {G : Game A} {p : Player} {x y : List A} (xy : x <+: y) (h : WinningPrefix G p x) : WinningPrefix G p y

theorem GaleStewartGame.PreStrategy.WinningPrefix.of_prefix' {A : Type u_1} {G : Game A} {p : Player} {x : List A} {G' : Game A} {p' : Player} {y : List A} (xy : x <+: y) (hG : G = G') (hp : p = p') (h : WinningPrefix G p x) : WinningPrefix G' p' y

theorem GaleStewartGame.PreStrategy.WinningPrefix.extend_num {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) (y : List A) : ⋯.num = h.num

theorem GaleStewartGame.PreStrategy.WinningPrefix.prefix_num {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {G' : Game A} {p' : Player} {y : List A} (xy : x <+: y) (hG : G = G') (hp : p = p') : ⋯.num = h.num

noncomputable def GaleStewartGame.PreStrategy.WinningPrefix.strat {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : Strategy (G.residual (List.take h.num x)).tree (Player.residual (List.take h.num x) p)

the winning strategy chosen for the shortest winning prefix of x

Equations

• h.strat = Exists.choose ⋯

theorem GaleStewartGame.PreStrategy.WinningPrefix.strat_winning {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : h.strat.pre.IsWinning

theorem GaleStewartGame.PreStrategy.WinningPrefix.extracted_1 {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} : Strategy (G.residual (List.take ⋯.num (x ++ y))).tree (Player.residual (List.take ⋯.num (x ++ y)) p) = Strategy (G.residual (List.take h.num x)).tree (Player.residual (List.take h.num x) p)

theorem GaleStewartGame.PreStrategy.WinningPrefix.extracted_2 {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} (a : Strategy (G.residual (List.take ⋯.num (x ++ y))).tree (Player.residual (List.take ⋯.num (x ++ y)) p)) : a.pre.IsWinning ↔ (cast ⋯ a).pre.IsWinning

theorem GaleStewartGame.PreStrategy.WinningPrefix.extend_strat {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) (y : List A) : ⋯.strat ≍ h.strat

theorem GaleStewartGame.PreStrategy.WinningPrefix.extend_strat_subtree {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) (y : List A) : ⋯.strat.pre.subtree = h.strat.pre.subtree

theorem GaleStewartGame.PreStrategy.WinningPrefix.prefix_strat_subtree {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {G' : Game A} {p' : Player} {y : List A} (xy : x <+: y) (hG : G = G') (hp : p = p') : ⋯.strat.pre.subtree = h.strat.pre.subtree

theorem GaleStewartGame.PreStrategy.WinningPrefix.strat_eval_val_congr {A : Type u_1} {p p' : Player} (U U' : ↥(Descriptive.tree A)) (hU : U = U') (hep : p = p') (S : Strategy U p) (S' : Strategy U' p') (h : S ≍ S') (x : ↥U) (hp : IsPosition (↑x) p) : ↑(S x hp) = ↑(S' ⟨↑x, ⋯⟩ ⋯)

theorem GaleStewartGame.PreStrategy.WinningPrefix.prefix_strat_apply {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {G' : Game A} {p' : Player} {y : List A} (xy : x <+: y) (hG : G = G') (hp : p = p') {a : ↥(G'.residual (List.take ⋯.num y)).tree} (hpa : IsPosition (↑a) (Player.residual (List.take ⋯.num y) p')) : have xy' := ⋯; ↑(⋯.strat a hpa) = ↑(h.strat ⟨↑a, ⋯⟩ ⋯)

theorem GaleStewartGame.PreStrategy.WinningPrefix.prefix_strat_apply' {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {G' : Game A} {p' : Player} {y : List A} (xy : x <+: y) (hG : G = G') (hp : p = p') {a : ↥(G'.residual (List.take ⋯.num y)).tree} {a' : ↥(G.residual (List.take h.num x)).tree} (ha : ↑a = ↑a') (hpa : IsPosition (↑a) (Player.residual (List.take ⋯.num y) p')) : have xy' := ⋯; ↑(⋯.strat a hpa) = ↑(h.strat a' ⋯)

theorem GaleStewartGame.PreStrategy.WinningPrefix.shrink {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : WinningPrefix G p (List.take h.num x)

Auxiliary declaration for the Borel determinacy formalization.

theorem GaleStewartGame.PreStrategy.WinningPrefix.shrink_num {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : ⋯.num = h.num

theorem GaleStewartGame.PreStrategy.WinningPrefix.shrink_strat {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) : ⋯.strat ≍ h.strat

theorem GaleStewartGame.PreStrategy.WinningPrefix.lem1 {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} : List.take ⋯.num (List.take h.num x ++ y) = List.take h.num x

theorem GaleStewartGame.PreStrategy.WinningPrefix.lem2 {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} : List.drop ⋯.num (List.take h.num x ++ y) = y

theorem GaleStewartGame.PreStrategy.WinningPrefix.val_cast {A : Type u_1} {x : List A} {T : ↥(Descriptive.tree A)} {y : List A} (h : x = y) (a : ↥(Descriptive.Tree.subAt T x)) (b : ↥(Descriptive.Tree.subAt T y)) : cast ⋯ a = b ↔ ↑a = ↑b

theorem GaleStewartGame.PreStrategy.WinningPrefix.val_cast' {A : Type u_1} {T T' : ↥(Descriptive.tree A)} {b : ↥T} {b' : ↥T'} (hT : T = T') (h : b = cast ⋯ b') (x : Descriptive.Tree.ExtensionsAt b) (y : Descriptive.Tree.ExtensionsAt b') : cast ⋯ x = y ↔ ↑x = ↑y

theorem GaleStewartGame.PreStrategy.WinningPrefix.cast_val {A : Type u_1} {x : List A} {T : ↥(Descriptive.tree A)} {y : List A} (h : x = y) (a : ↥(Descriptive.Tree.subAt T x)) : ↑(cast ⋯ a) = ↑a

theorem GaleStewartGame.PreStrategy.WinningPrefix.hEq_drop_take {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} (hy : y ∈ Descriptive.Tree.subAt G.tree (List.take h.num x)) (hxy : List.take h.num x ++ y ∈ G.tree) : Descriptive.Tree.drop G.tree ⋯.num ⟨List.take h.num x ++ y, hxy⟩ ≍ ⟨y, hy⟩

theorem GaleStewartGame.PreStrategy.WinningPrefix.congr_2_heq {α α' : Sort u_2} {β : α → Prop} {γ : α → Type u} {β' : α → Prop} {γ' : α → Type u} {a : α} {a' : α'} (ha : a ≍ a') (f : (a : α) → β a → γ a) (f' : (a'' : α') → β' (cast ⋯ a'') → γ' (cast ⋯ a'')) (b : β a) (b' : β' (cast ⋯ a')) (hb : β = β') (hct : γ = γ') (hf : f ≍ f') : f a b ≍ f' a' b'

theorem GaleStewartGame.PreStrategy.WinningPrefix.congr_2_heq' {α α' : Sort u_2} {β : α → Prop} {γ : α → Type u} {β' : α' → Prop} {γ' : α' → Type u} {a : α} {a' : α'} (ha : a ≍ a') (f : (a : α) → β a → γ a) (f' : (a' : α') → β' a' → γ' a') (b : β a) (b' : β' (cast ⋯ a')) (hB : β ≍ β') (hC : γ ≍ γ') (hf : f ≍ f') : f a b ≍ f' a' b'

theorem GaleStewartGame.PreStrategy.WinningPrefix.extend_strat_apply {A : Type u_1} {G : Game A} {p : Player} {x : List A} (h : WinningPrefix G p x) {y : List A} {a : ↥(G.residual (List.take ⋯.num (List.take h.num x ++ y))).tree} {a' : ↥(G.residual (List.take h.num x)).tree} (ha : a ≍ a') {hpa : IsPosition (↑a) (Player.residual (List.take ⋯.num (List.take h.num x ++ y)) p)} {hpa' : IsPosition (↑a') (Player.residual (List.take h.num x) p)} : ↑(⋯.strat a hpa) = ↑(h.strat a' hpa')

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.PreStrategy.mem_winAsap_subtree_of_no_prefix {A : Type u_1} (G : Game A) (p : Player) {x : List A} {a : A} (h : ¬WinningPrefix G p x) (ha : x ++ [a] ∈ G.tree) : x ++ [a] ∈ (winAsap G p).subtree

theorem GaleStewartGame.PreStrategy.winAsap_subtree {A : Type u_1} (G : Game A) (p : Player) {x : List A} (h : WinningPrefix G p x) : Descriptive.Tree.subAt (winAsap G p).subtree (List.take h.num x) = h.strat.pre.subtree

theorem GaleStewartGame.PreStrategy.winAsap_body {A : Type u_1} (G : Game A) (p : Player) (x : ↑(Descriptive.Tree.body (winAsap G p).subtree)) (h : ∃ (n : ℕ), WinningPrefix G p (Stream'.take n ↑x)) : ⟨↑x, ⋯⟩ ∈ p.payoff G

theorem GaleStewartGame.PreStrategy.winAsap_body' {A : Type u_1} (G : Game A) (p : Player) (x : ↑(Descriptive.Tree.body (winAsap G p).followUntilWon.subtree)) (h : ∃ (n : ℕ), WinningPrefix G p (Stream'.take n ↑x)) : ⟨↑x, ⋯⟩ ∈ p.payoff G