Small games all around

We define dicotic games, games x where both players can move from every nonempty subposition of x. We prove that these games are small, and relate them to infinitesimals.

TODO

• Define infinitesimal games as games x such that ∀ r : ℝ, 0 < r → -r < x ∧ x < r
  • (Does this hold for small infinitesimal games?)
• Prove that any short dicotic game is an infinitesimal (but not vice versa, consider ω⁻¹)

Dicotic games

class IGame.Dicotic (x : IGame) : Prop

A game x is dicotic if both players can move from every nonempty subposition of x.

• of_DicoticAux :: (
• out : IGame.DicoticAux✝ x
• )

theorem IGame.dicotic_iff_aux (x : IGame) : x.Dicotic ↔ IGame.DicoticAux✝ x

theorem IGame.dicotic_def {x : IGame} : x.Dicotic ↔ (moves left x = ∅ ↔ moves right x = ∅) ∧ ∀ (p : Player), ∀ l ∈ moves p x, l.Dicotic

theorem IGame.Dicotic.mk {x : IGame} (h₁ : moves left x = ∅ ↔ moves right x = ∅) (h₂ : ∀ (p : Player), ∀ y ∈ moves p x, y.Dicotic) : x.Dicotic

theorem IGame.Dicotic.eq_zero_iff {x : IGame} [hx : x.Dicotic] : x = 0 ↔ ∃ (p : Player), moves p x = ∅

theorem IGame.Dicotic.ne_zero_iff {x : IGame} [x.Dicotic] : x ≠ 0 ↔ ∀ (p : Player), moves p x ≠ ∅

theorem IGame.Dicotic.moves_eq_empty_iff {x : IGame} [hx : x.Dicotic] (p q : Player) : moves p x = ∅ ↔ moves q x = ∅

theorem IGame.Dicotic.of_mem_moves {x y : IGame} {p : Player} [hx : x.Dicotic] (h : y ∈ moves p x) : y.Dicotic

def IGame.Dicotic.tacticDicotic : Lean.ParserDescr

dicotic eagerly adds all possible Dicotic hypotheses.

Equations

• IGame.Dicotic.tacticDicotic = Lean.ParserDescr.node `IGame.Dicotic.tacticDicotic 1024 (Lean.ParserDescr.nonReservedSymbol "dicotic" false)

@[simp]

instance IGame.Dicotic.zero : Dicotic 0

@[irreducible]

instance IGame.Dicotic.neg (x : IGame) [x.Dicotic] : (-x).Dicotic

@[irreducible]

theorem IGame.Dicotic.lt_of_numeric_of_pos (x : IGame) [x.Dicotic] {y : IGame} [y.Numeric] (hy : 0 < y) : x < y

One half of the lawnmower theorem: any dicotic game is smaller than any positive numeric game.

theorem IGame.Dicotic.lt_of_numeric_of_neg (x : IGame) [x.Dicotic] {y : IGame} [y.Numeric] (hy : y < 0) : y < x

One half of the lawnmower theorem: any dicotic game is greater than any negative numeric game.