LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet

Auxiliary declarations for the Borel determinacy formalization.

def Choquet.chainTree {X : Type u_1} (V : Set (Set X)) : ↥(Descriptive.tree ↑V)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.chainTree V = ⟨{x : List ↑V | List.IsChain (fun (x1 x2 : ↑V) => x1 ≥ x2) x}, ⋯⟩

theorem Choquet.def_chainTree {X : Type u_1} (V : Set (Set X)) (x : List ↑V) : x ∈ chainTree V ↔ List.IsChain (fun (x1 x2 : ↑V) => x1 ≥ x2) x

theorem Choquet.nil_mem_chainTree {X : Type u_1} (V : Set (Set X)) : [] ∈ chainTree V

theorem Choquet.concat_mem_chainTree {X : Type u_1} (V : Set (Set X)) {x : List ↑V} {A : ↑V} : x ++ [A] ∈ chainTree V ↔ x ∈ chainTree V ∧ ∀ (hx : x ≠ []), A ≤ x.getLast hx

def Choquet.chainTree.concat {X : Type u_1} (V : Set (Set X)) (x : ↥(chainTree V)) (A : ↑V) (h : ∀ (hx : ↑x ≠ []), A ≤ (↑x).getLast hx) : ↥(chainTree V)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.chainTree.concat V x A h = ⟨↑x ++ [A], ⋯⟩

def Choquet.interGame {X : Type u_1} (V PO : Set (Set X)) : GaleStewartGame.Game ↑V

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.interGame V PO = { tree := Choquet.chainTree V, payoff := fun (A : ↑(Descriptive.Tree.body (Choquet.chainTree V))) => PO (⋂ (n : ℕ), ↑(↑A n)) }

theorem Choquet.extend_mem_iff {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) (x : List ↑W) : List.map (Set.inclusion hWV) x ∈ chainTree V ↔ x ∈ chainTree W

def Choquet.extend {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) (x : ↥(chainTree W)) : ↥(chainTree V)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.extend hWV x = ⟨List.map (Set.inclusion hWV) ↑x, ⋯⟩

@[simp]

theorem Choquet.extend_coe {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) (x : ↥(chainTree W)) : ↑(extend hWV x) = List.map (Set.inclusion hWV) ↑x

def Choquet.extend' {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) {x : ↥(chainTree W)} (a : Descriptive.Tree.ExtensionsAt x) : Descriptive.Tree.ExtensionsAt (extend hWV x)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.extend' hWV a = ⟨Set.inclusion hWV ↑a, ⋯⟩

@[simp]

theorem Choquet.extend'_coe_coe {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) {x : ↥(chainTree W)} (a : Descriptive.Tree.ExtensionsAt x) : ↑↑(extend' hWV a) = ↑↑a

def Choquet.choosePair {X : Type u_1} {V W : Set (Set X)} (hW : ∀ A ∈ V, ∃ B ∈ W, B ⊆ A) (A : ↑V) : ↑W

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.choosePair hW A = ⟨⋯.choose, ⋯⟩

theorem Choquet.choosePairSub {X : Type u_1} {V W : Set (Set X)} (hW : ∀ A ∈ V, ∃ B ∈ W, B ⊆ A) (A : ↑V) : ↑(choosePair hW A) ⊆ ↑A

def Choquet.shrink' {X : Type u_1} {V W : Set (Set X)} (hWV : W ⊆ V) (hW : ∀ A ∈ V, ∃ B ∈ W, B ⊆ A) {x : ↥(chainTree W)} (a : Descriptive.Tree.ExtensionsAt (extend hWV x)) : Descriptive.Tree.ExtensionsAt x

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.shrink' hWV hW a = ⟨Choquet.choosePair hW ↑a, ⋯⟩

def Choquet.game (X : Type u_1) [TopologicalSpace X] : GaleStewartGame.Game ↑{A : Set X | IsOpen A ∧ A.Nonempty}

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.game X = Choquet.interGame {A : Set X | IsOpen A ∧ A.Nonempty} {∅}

def Choquet.IsChoquet (X : Type u_1) [TopologicalSpace X] : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Choquet.IsChoquet X = (Choquet.game X).ExistsWinning GaleStewartGame.Player.one