Documentation

CombinatorialGames.Game.Birthday

Birthdays of games #

There are two related but distinct notions of a birthday within combinatorial game theory. One is the birthday of an IGame, which represents the "step" at which it is constructed. We define it recursively as the least ordinal larger than the birthdays of its left and right options. On the other hand, the birthday of a Game is the smallest birthday among all IGames that quotient to it.

The birthday of an IGame can be understood as representing the depth of its game tree. Meanwhile, the birthday of a Game more closely matches Conway's original description. The lemma Game.birthday_eq_iGameBirthday links both definitions together.

Stuff for Mathlib #

theorem ciSup_eq_bot {α : Type u_1} {ι : Sort u_2} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} (hf : BddAbove (Set.range f)) :

⨆ (i : ι), f i = ⊥ ↔ ∀ (i : ι), f i = ⊥

@[simp]

theorem Set.empty_ne_singleton {α : Type u_1} (a : α) :

@[simp]

theorem NatOrdinal.bot_eq_zero' :

@[simp]

theorem NatOrdinal.succ_ne_zero (x : NatOrdinal) :

Order.succ x ≠ 0

@[simp]

theorem NatOrdinal.le_zero {x : NatOrdinal} :

x ≤ 0 ↔ x = 0

@[simp]

theorem NatOrdinal.succ_zero :

Order.succ 0 = 1

@[simp]

theorem NatOrdinal.succ_one :

Order.succ 1 = 2

theorem NatOrdinal.lt_iSup_iff {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → NatOrdinal) {x : NatOrdinal} :

x < ⨆ (i : ι), f i ↔ ∃ (i : ι), x < f i

theorem NatOrdinal.iSup_eq_zero_iff {ι : Type u_1} [Small.{u, u_1} ι] {f : ι → NatOrdinal} :

⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

theorem NatOrdinal.lt_omega0 {o : NatOrdinal} :

o < Ordinal.toNatOrdinal Ordinal.omega0 ↔ ∃ (n : ℕ), o = ↑n

theorem NatOrdinal.nat_lt_omega0 (n : ℕ) :

↑n < Ordinal.toNatOrdinal Ordinal.omega0

`IGame` birthday #

@[irreducible]

noncomputable def IGame.birthday (x : IGame) :

The birthday of an IGame is inductively defined as the least strict upper bound of the birthdays of its options. It may be thought as the "step" in which a certain game is constructed.

Equations

x.birthday = ⨆ (y : { y : IGame // y.IsOption x }), Order.succ (↑y).birthday

Instances For

theorem IGame.lt_birthday_iff' {x : IGame} {o : NatOrdinal} :

o < x.birthday ↔ ∃ (y : IGame), y.IsOption x ∧ o ≤ y.birthday

theorem IGame.birthday_le_iff' {x : IGame} {o : NatOrdinal} :

x.birthday ≤ o ↔ ∀ (y : IGame), y.IsOption x → y.birthday < o

theorem IGame.lt_birthday_iff {x : IGame} {o : NatOrdinal} :

o < x.birthday ↔ (∃ y ∈ x.leftMoves, o ≤ y.birthday) ∨ ∃ y ∈ x.rightMoves, o ≤ y.birthday

theorem IGame.birthday_le_iff {x : IGame} {o : NatOrdinal} :

x.birthday ≤ o ↔ (∀ y ∈ x.leftMoves, y.birthday < o) ∧ ∀ y ∈ x.rightMoves, y.birthday < o

theorem IGame.birthday_eq_max (x : IGame) :

x.birthday = max (⨆ (y : ↑x.leftMoves), Order.succ (↑y).birthday) (⨆ (y : ↑x.rightMoves), Order.succ (↑y).birthday)

theorem IGame.birthday_lt_of_mem_leftMoves {x y : IGame} (hy : y ∈ x.leftMoves) :

y.birthday < x.birthday

theorem IGame.birthday_lt_of_mem_rightMoves {x y : IGame} (hy : y ∈ x.rightMoves) :

y.birthday < x.birthday

theorem IGame.birthday_lt_of_isOption {x y : IGame} (hy : y.IsOption x) :

y.birthday < x.birthday

@[irreducible]

theorem IGame.birthday_lt_of_subposition {x y : IGame} (hy : y.Subposition x) :

y.birthday < x.birthday

theorem IGame.birthday_ofSets (s t : Set IGame) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] :

{s | t}ᴵ.birthday = max (sSup (Order.succ ∘ birthday '' s)) (sSup (Order.succ ∘ birthday '' t))

@[simp]

theorem IGame.birthday_eq_zero {x : IGame} :

x.birthday = 0 ↔ x = 0

@[simp]

theorem IGame.birthday_zero :

@[simp]

theorem IGame.birthday_one :

@[simp]

theorem IGame.birthday_star :

⋆.birthday = 1

@[simp]

theorem IGame.birthday_half :

½.birthday = 2

@[simp]

theorem IGame.birthday_up :

↑.birthday = 2

@[simp]

theorem IGame.birthday_down :

↓.birthday = 2

@[simp, irreducible]

theorem IGame.birthday_neg (x : IGame) :

(-x).birthday = x.birthday

@[simp, irreducible]

theorem IGame.birthday_toIGame (o : NatOrdinal) :

(NatOrdinal.toIGame o).birthday = o

@[irreducible]

theorem IGame.le_toIGame_birthday (x : IGame) :

x ≤ NatOrdinal.toIGame x.birthday

theorem IGame.neg_toIGame_birthday_le (x : IGame) :

-NatOrdinal.toIGame x.birthday ≤ x

@[simp, irreducible]

theorem IGame.birthday_add (x y : IGame) :

(x + y).birthday = x.birthday + y.birthday

@[simp]

theorem IGame.birthday_sub (x y : IGame) :

(x - y).birthday = x.birthday + y.birthday

@[simp]

theorem IGame.birthday_natCast (n : ℕ) :

(↑n).birthday = ↑n

@[simp]

theorem IGame.birthday_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).birthday = ↑n

@[simp]

theorem IGame.birthday_tiny (x : IGame) :

(⧾x).birthday = x.birthday + 2

@[simp]

theorem IGame.birthday_miny (x : IGame) :

(⧿x).birthday = x.birthday + 2

@[irreducible]

instance IGame.small_setOf_birthday_le (o : NatOrdinal) :

Small.{u, u + 1} { x : IGame // x.birthday ≤ o }

Games with a bounded birthday form a small set.

instance IGame.small_setOf_birthday_lt (o : NatOrdinal) :

Small.{u, u + 1} { x : IGame // x.birthday < o }

Games with a bounded birthday form a small set.

Short games #

noncomputable def IGame.birthdayFinset :

ℕ → Finset IGame

The finset of all games with birthday ≤ n.

Equations

One or more equations did not get rendered due to their size.
IGame.birthdayFinset 0 = {0}

Instances For

theorem IGame.mem_birthdayFinset_succ {x : IGame} {n : ℕ} :

x ∈ birthdayFinset (n + 1) ↔ ∃ (l : Finset IGame) (r : Finset IGame), (l ⊆ birthdayFinset n ∧ r ⊆ birthdayFinset n) ∧ {↑l | ↑r}ᴵ = x

@[simp]

theorem IGame.birthdayFinset_zero :

birthdayFinset 0 = {0}

theorem IGame.birthdayFinset_one :

birthdayFinset 1 = { val := ↑[0, 1, -1, ⋆], nodup := ⋯ }

@[simp]

theorem IGame.card_birthdayFinset (n : ℕ) :

(birthdayFinset (n + 1)).card = 4 ^ (birthdayFinset n).card

theorem IGame.mem_birthdayFinset_of_isOption {x y : IGame} {n : ℕ} (hnx : x ∈ birthdayFinset (n + 1)) (hy : y.IsOption x) :

y ∈ birthdayFinset n

@[simp]

theorem IGame.mem_birthdayFinset {x : IGame} {n : ℕ} :

x ∈ birthdayFinset n ↔ x.birthday ≤ ↑n

theorem IGame.strictMono_birthdayFinset :

StrictMono birthdayFinset

@[irreducible]

theorem IGame.short_iff_birthday_finite {x : IGame} :

x.Short ↔ x.birthday < Ordinal.toNatOrdinal Ordinal.omega0

`Game` birthday #

noncomputable def Game.birthday (x : Game) :

The birthday of a game is defined as the least birthday among all pre-games that define it.

Equations

x.birthday = sInf (IGame.birthday '' (Game.mk ⁻¹' {x}))

Instances For

theorem Game.birthday_eq_iGameBirthday (x : Game) :

∃ (y : IGame), mk y = x ∧ y.birthday = x.birthday

theorem Game.birthday_mk_le (x : IGame) :

(mk x).birthday ≤ x.birthday

@[simp]

theorem Game.birthday_zero :

@[simp]

theorem Game.birthday_eq_zero {x : Game} :

x.birthday = 0 ↔ x = 0

@[simp]

theorem Game.birthday_neg (x : Game) :

(-x).birthday = x.birthday

theorem Game.le_toGame_birthday (x : Game) :

x ≤ NatOrdinal.toGame x.birthday

theorem Game.neg_toGame_birthday_le (x : Game) :

-NatOrdinal.toGame x.birthday ≤ x

@[simp]

theorem Game.birthday_toGame (o : NatOrdinal) :

(NatOrdinal.toGame o).birthday = o

@[simp]

theorem Game.birthday_natCast (n : ℕ) :

(↑n).birthday = ↑n

@[simp]

theorem Game.birthday_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).birthday = ↑n

@[simp]

theorem Game.birthday_one :

@[simp]

theorem Game.birthday_star :

(mk ⋆).birthday = 1

theorem Game.birthday_add_le (x y : Game) :

(x + y).birthday ≤ x.birthday + y.birthday

theorem Game.birthday_sub_le (x y : Game) :

(x - y).birthday ≤ x.birthday + y.birthday

instance Game.small_setOf_birthday_le (o : NatOrdinal) :

Small.{u, u + 1} { x : Game // x.birthday ≤ o }

Games with a bounded birthday form a small set.

instance Game.small_setOf_birthday_lt (o : NatOrdinal) :

Small.{u, u + 1} { x : Game // x.birthday < o }

Games with a bounded birthday form a small set.