LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy

Auxiliary declarations for the Borel determinacy formalization.

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.Gh {A : Type} {G : Game A} {k : ℕ} (hyp : Hyp G k) : Covering.Games

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.Gh hyp = ⟨A, ⟨G, ⋯⟩⟩

@[reducible, inline]

abbrev GaleStewartGame.BorelDet.G'h {A : Type} {G : Game A} {k : ℕ} (hyp : Hyp G k) : Covering.Games

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.G'h hyp = ⟨GaleStewartGame.BorelDet.A', ⟨GaleStewartGame.BorelDet.G', ⋯⟩⟩

noncomputable def GaleStewartGame.BorelDet.treeCov {A : Type} {G : Game A} {k : ℕ} (hyp : Hyp G k) : (G'h hyp).tree ⟶ (Gh hyp).tree

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

noncomputable def GaleStewartGame.BorelDet.gameCov {A : Type} {G : Game A} {k : ℕ} (hyp : Hyp G k) : (G'h hyp).Covering (Gh hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet.gameCov hyp = { toCovering := GaleStewartGame.BorelDet.treeCov hyp, hpre := ⋯ }

theorem GaleStewartGame.BorelDet.main_lemma {G : Covering.Games} (hC : IsClosed G.snd.fst.payoff) : G.IsUnravelable

def GaleStewartGame.BorelDet'.extendToGame (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) : Covering.Games

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet'.extendToGame T W = ⟨T.fst.fst, ⟨{ tree := T.fst.snd, payoff := W }, ⋯⟩⟩

@[simp]

theorem GaleStewartGame.BorelDet'.extendToGame_fst (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) : (extendToGame T W).fst = T.fst.fst

@[simp]

theorem GaleStewartGame.BorelDet'.extendToGame_snd_fst_payoff (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) : (extendToGame T W).snd.fst.payoff = W

@[simp]

theorem GaleStewartGame.BorelDet'.extendToGame_snd_fst_tree (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) : (extendToGame T W).snd.fst.tree = T.fst.snd

def GaleStewartGame.BorelDet'.UniversallyUnravelable (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) : Prop

a slight strengthening of Martin's notion of unravelable games to facilitate Borel induction

Equations

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

theorem GaleStewartGame.BorelDet'.unravelable_complement (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) (h : UniversallyUnravelable T W) : UniversallyUnravelable T Wᶜ

theorem GaleStewartGame.BorelDet'.closed_unravelable (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) (h : IsClosed W) : UniversallyUnravelable T W

theorem GaleStewartGame.BorelDet'.open_unravelable (T : Covering.PTrees) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) (h : IsOpen W) : UniversallyUnravelable T W

theorem GaleStewartGame.BorelDet'.unravelable_preimage {T' T : Covering.PTrees} (f : T' ⟶ T) (W : Set ↑(Descriptive.Tree.body T.fst.snd)) (h : UniversallyUnravelable T W) : UniversallyUnravelable T' (⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map f.toHom)) ⁻¹' W)

structure GaleStewartGame.BorelDet'.PartiallyUnravelled (n : ℕ) : Type 1

Auxiliary declaration for the Borel determinacy formalization.

• carrier : Covering.PTrees

  Auxiliary declaration for the Borel determinacy formalization.

• sets : ℕ → PSigma (UniversallyUnravelable self.carrier)

  Auxiliary declaration for the Borel determinacy formalization.

• unrav (m : ℕ) : m < n → IsOpen (self.sets m).fst

noncomputable def GaleStewartGame.BorelDet'.PartiallyUnravelled.continue {n : ℕ} (G : PartiallyUnravelled n) (k : ℕ) : (G' : PartiallyUnravelled (n + 1)) ×' (f : G'.carrier ⟶ G.carrier) ×' Covering.Fixing (k + n) f ∧ ∀ (n_1 : ℕ), (G'.sets n_1).fst = ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map f.toHom)) ⁻¹' (G.sets n_1).fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

• G.continue k = Classical.choice ⋯

def GaleStewartGame.BorelDet'.unravelNth (G : PartiallyUnravelled 0) (k n : ℕ) : PartiallyUnravelled n

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet'.unravelNth G k 0 = G
• GaleStewartGame.BorelDet'.unravelNth G k n.succ = ((GaleStewartGame.BorelDet'.unravelNth G k n).continue k).fst

noncomputable def GaleStewartGame.BorelDet'.unravelFunctor (G : PartiallyUnravelled 0) (k : ℕ) : CategoryTheory.Functor ℕᵒᵖ Covering.PTrees

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.BorelDet'.unravelFunctor_succ (G : PartiallyUnravelled 0) (k n : ℕ) : (unravelFunctor G k).map (CategoryTheory.homOfLE ⋯).op = ((unravelNth G k n).continue k).snd.fst

theorem GaleStewartGame.BorelDet'.unravelFunctor_fixing (G : PartiallyUnravelled 0) (k n : ℕ) : Covering.Fixing (k + n) ((unravelFunctor G k).map (CategoryTheory.homOfLE ⋯).op)

theorem GaleStewartGame.BorelDet'.unravelFunctor_preimage (G : PartiallyUnravelled 0) (k m n : ℕ) : ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map ((unravelFunctor G k).map (CategoryTheory.homOfLE ⋯).op).toHom)) ⁻¹' (G.sets m).fst = ((unravelNth G k n).sets m).fst

noncomputable def GaleStewartGame.BorelDet'.unravelLim (G : PartiallyUnravelled 0) (k : ℕ) : CategoryTheory.Limits.Cone (unravelFunctor G k)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• GaleStewartGame.BorelDet'.unravelLim G k = GaleStewartGame.Covering.limCone ⋯

theorem GaleStewartGame.BorelDet'.unravelLim_fixing (G : PartiallyUnravelled 0) (k : ℕ) : Covering.Fixing k ((unravelLim G k).π.app (Opposite.op 0))

@[reducible]

def GaleStewartGame.BorelDet'.unravelableAsMeasurable (T : Covering.PTrees) : MeasurableSpace ↑(Descriptive.Tree.body T.fst.snd)

the σ-algebra of universally unravelable sets

Equations

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

theorem GaleStewartGame.BorelDet'.borel_unravelable (T : Covering.PTrees) : borel ↑(Descriptive.Tree.body T.fst.snd) ≤ unravelableAsMeasurable T

theorem GaleStewartGame.Games.borel_determinacy (G : Covering.Games) (h : MeasurableSet G.snd.fst.payoff) : G.snd.fst.IsDetermined

Borel games are determined

theorem GaleStewartGame.borel_determinacy {A : Type} {G : Game A} (hB : MeasurableSet G.payoff) (hP : Descriptive.Tree.IsPruned G.tree) : G.IsDetermined