Documentation

CombinatorialGames.NatOrdinal

Natural operations on ordinals #

The goal of this file is to define natural addition and multiplication on ordinals, also known as the Hessenberg sum and product, and provide a basic API. The natural addition of two ordinals a + b is recursively defined as the least ordinal greater than a' + b and a + b' for a' < a and b' < b. The natural multiplication a * b is likewise recursively defined as the least ordinal such that a * b + a' * b' is greater than a' * b + a * b' for any a' < a and b' < b.

These operations give the ordinals a CommSemiring + IsStrictOrderedRing structure. To make the best use of it, we define them on a type alias NatOrdinal.

An equivalent characterization explains the relevance of these operations to game theory: they are the restrictions of surreal addition and multiplication to the ordinals.

Implementation notes #

To reduce API duplication, we opt not to implement operations on NatOrdinal on Ordinal. The order isomorphisms NatOrdinal.of and NatOrdinal.val allow us to cast between them whenever needed.

For similar reasons, most results about ordinals and games are written using NatOrdinal rather than Ordinal (except when Nimber would make more sense).

Todo #

Prove the characterizations of natural addition and multiplication in terms of the Cantor normal form.

Basic casts between `Ordinal` and `NatOrdinal` #

instance instNatOrdinalZero :

Zero NatOrdinal

Equations

instNatOrdinalZero = Ordinal.zero

instance NatOrdinal.instIsEmptyElemIioOfNat :

IsEmpty ↑(Set.Iio 0)

theorem NatOrdinal.bddAbove_of_small (s✝ : Set NatOrdinal) [Small.{u✝, u✝ + 1} ↑s✝] :

@[simp]

theorem NatOrdinal.val_symm :

@[simp]

theorem NatOrdinal.of_image_Iio (a✝ : Ordinal.{u_1}) :

⇑of '' Set.Iio a✝ = Set.Iio (of a✝)

theorem NatOrdinal.not_bddAbove_compl_of_small (s✝ : Set NatOrdinal) [Small.{u✝, u✝ + 1} ↑s✝] :

¬BddAbove s✝ᶜ

@[simp]

theorem NatOrdinal.val_eq_zero {a✝ : NatOrdinal} :

val a✝ = 0 ↔ a✝ = 0

theorem NatOrdinal.succ_def (a✝ : NatOrdinal) :

Order.succ a✝ = of (val a✝ + 1)

theorem NatOrdinal.val_le_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ ≤ b✝ ↔ a✝ ≤ of b✝

@[simp]

theorem NatOrdinal.of_zero :

of 0 = 0

instance instNatOrdinalOne :

Equations

instNatOrdinalOne = Ordinal.one

instance NatOrdinal.instSmallElemIoo (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ioo a✝ b✝)

instance NatOrdinal.instSuccOrder :

SuccOrder NatOrdinal

Equations

NatOrdinal.instSuccOrder = Ordinal.instSuccOrder

instance NatOrdinal.instSmallElemIio (a✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Iio a✝)

@[simp]

theorem NatOrdinal.of_val (a✝ : NatOrdinal) :

of (val a✝) = a✝

@[simp]

theorem NatOrdinal.Iio_one_default_eq :

default = ⟨0, ⋯⟩

@[simp]

theorem NatOrdinal.val_of (a✝ : Ordinal.{u_1}) :

val (of a✝) = a✝

@[simp]

theorem NatOrdinal.of_eq_zero {a✝ : Ordinal.{u_1}} :

of a✝ = 0 ↔ a✝ = 0

instance instNatOrdinalNontrivial :

Nontrivial NatOrdinal

Equations

instNatOrdinalNontrivial = Ordinal.nontrivial

noncomputable instance NatOrdinal.instLinearOrder :

LinearOrder NatOrdinal

Equations

NatOrdinal.instLinearOrder = Ordinal.instLinearOrder

@[match_pattern]

def NatOrdinal.val :

NatOrdinal ≃o Ordinal.{u_1}

The identity function between NatOrdinal and Ordinal.

Equations

NatOrdinal.val = OrderIso.refl NatOrdinal

Instances For

@[simp]

theorem NatOrdinal.bot_eq_zero :

theorem NatOrdinal.lt_wf :

WellFounded fun (x1 x2 : NatOrdinal) => x1 < x2

@[simp]

theorem NatOrdinal.not_lt_zero (a✝ : NatOrdinal) :

¬a✝ < 0

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

⨆ (i : ι✝), f✝ i ≤ a✝ ↔ ∀ (i : ι✝), f✝ i ≤ a✝

@[simp]

theorem NatOrdinal.succ_of (a✝ : Ordinal.{u_1}) :

Order.succ (of a✝) = of (a✝ + 1)

@[simp]

theorem NatOrdinal.of_symm :

theorem NatOrdinal.induction {p✝ : NatOrdinal → Prop} (i✝ : NatOrdinal) :

(∀ (j : NatOrdinal), (∀ k < j, p✝ k) → p✝ j) → p✝ i✝

Ordinal.induction but for NatOrdinal.

@[simp]

theorem NatOrdinal.one_le_iff_ne_zero {a✝ : NatOrdinal} :

1 ≤ a✝ ↔ a✝ ≠ 0

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

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

@[simp]

theorem NatOrdinal.of_eq_one {a✝ : Ordinal.{u_1}} :

of a✝ = 1 ↔ a✝ = 1

instance NatOrdinal.instUncountable :

Uncountable NatOrdinal

instance NatOrdinal.instUniqueElemIioOfNat :

Unique ↑(Set.Iio 1)

Equations

NatOrdinal.instUniqueElemIioOfNat = Ordinal.uniqueIioOne

@[simp]

theorem NatOrdinal.val_eq_one {a✝ : NatOrdinal} :

val a✝ = 1 ↔ a✝ = 1

@[simp]

theorem NatOrdinal.val_image_Iio (a✝ : NatOrdinal) :

⇑val '' Set.Iio a✝ = Set.Iio (val a✝)

theorem NatOrdinal.pos_iff_ne_zero {a✝ : NatOrdinal} :

0 < a✝ ↔ a✝ ≠ 0

theorem NatOrdinal.bddAbove_iff_small {s✝ : Set NatOrdinal} :

BddAbove s✝ ↔ Small.{u✝, u✝ + 1} ↑s✝

@[simp]

theorem NatOrdinal.le_zero {a✝ : NatOrdinal} :

a✝ ≤ 0 ↔ a✝ = 0

instance NatOrdinal.instSmallElemIoc (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ioc a✝ b✝)

@[simp]

theorem NatOrdinal.zero_le (a✝ : NatOrdinal) :

0 ≤ a✝

instance NatOrdinal.instSmallElemIcc (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Icc a✝ b✝)

instance NatOrdinal.instZeroLEOneClass :

ZeroLEOneClass NatOrdinal

instance NatOrdinal.instNoMaxOrder :

NoMaxOrder NatOrdinal

@[simp]

theorem NatOrdinal.succ_zero :

Order.succ 0 = 1

theorem NatOrdinal.eq_natCast_of_le_natCast {a✝ : NatOrdinal} {b✝ : ℕ} :

a✝ ≤ of ↑b✝ → ∃ (c : ℕ), a✝ = of ↑c

instance NatOrdinal.instWellFoundedLT :

WellFoundedLT NatOrdinal

@[simp]

theorem NatOrdinal.succ_ne_zero (a✝ : NatOrdinal) :

Order.succ a✝ ≠ 0

theorem NatOrdinal.of_lt_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ < b✝ ↔ a✝ < val b✝

def NatOrdinal :

Type (u_1 + 1)

A type synonym for ordinals with natural addition and multiplication.

Equations

NatOrdinal = Ordinal.{?u.2}

Instances For

instance NatOrdinal.instSmallElemIco (a✝ b✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Ico a✝ b✝)

instance NatOrdinal.instSmallElemIic (a✝ : NatOrdinal) :

Small.{u✝, u✝ + 1} ↑(Set.Iic a✝)

@[simp]

theorem NatOrdinal.of_one :

of 1 = 1

@[match_pattern]

def NatOrdinal.of :

Ordinal.{u_1} ≃o NatOrdinal

The identity function between Ordinal and NatOrdinal.

Equations

NatOrdinal.of = OrderIso.refl Ordinal.{?u.2}

Instances For

@[simp]

theorem NatOrdinal.val_one :

val 1 = 1

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

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

@[simp]

theorem NatOrdinal.val_zero :

val 0 = 0

instance NatOrdinal.instOrderBot :

OrderBot NatOrdinal

Equations

NatOrdinal.instOrderBot = Ordinal.instOrderBot

instance instNatOrdinalInhabited :

Inhabited NatOrdinal

Equations

instNatOrdinalInhabited = Ordinal.inhabited

instance NatOrdinal.instNeZeroOfNat :

theorem NatOrdinal.val_eq_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ = b✝ ↔ a✝ = of b✝

theorem NatOrdinal.of_le_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ ≤ b✝ ↔ a✝ ≤ val b✝

theorem NatOrdinal.le_iSup {ι✝ : Type u_1} (f✝ : ι✝ → NatOrdinal) [Small.{u✝, u_1} ι✝] (i✝ : ι✝) :

f✝ i✝ ≤ iSup f✝

instance instNatOrdinalWellFoundedRelation :

WellFoundedRelation NatOrdinal

Equations

instNatOrdinalWellFoundedRelation = Ordinal.wellFoundedRelation

noncomputable instance NatOrdinal.instConditionallyCompleteLinearOrderBot :

ConditionallyCompleteLinearOrderBot NatOrdinal

Equations

NatOrdinal.instConditionallyCompleteLinearOrderBot = Ordinal.instConditionallyCompleteLinearOrderBot

theorem NatOrdinal.val_lt_iff {a✝ : NatOrdinal} {b✝ : Ordinal.{u_1}} :

val a✝ < b✝ ↔ a✝ < of b✝

def NatOrdinal.ind {motive✝ : NatOrdinal → Sort u_1} (mk : (a : Ordinal.{u_2}) → motive✝ (of a)) (a✝ : NatOrdinal) :

motive✝ a✝

A recursor for NatOrdinal. Use as induction x.

Equations

NatOrdinal.ind mk a✝ = mk (NatOrdinal.val a✝)

Instances For

@[simp]

theorem NatOrdinal.lt_one_iff_zero {a✝ : NatOrdinal} :

a✝ < 1 ↔ a✝ = 0

theorem NatOrdinal.eq_zero_or_pos (a✝ : NatOrdinal) :

a✝ = 0 ∨ 0 < a✝

theorem NatOrdinal.le_one_iff {a✝ : NatOrdinal} :

a✝ ≤ 1 ↔ a✝ = 0 ∨ a✝ = 1

theorem NatOrdinal.of_eq_iff {a✝ : Ordinal.{u_1}} {b✝ : NatOrdinal} :

of a✝ = b✝ ↔ a✝ = val b✝

Natural addition #

@[irreducible]

noncomputable def NatOrdinal.add (a b : NatOrdinal) :

Natural addition on ordinals a + b, also known as the Hessenberg sum, is recursively defined as the least ordinal greater than a' + b and a + b' for all a' < a and b' < b. In contrast to normal ordinal addition, it is commutative.

Natural addition can equivalently be characterized as the ordinal resulting from adding up corresponding coefficients in the Cantor normal forms of a and b.

Equations

a.add b = max (⨆ (x : ↑(Set.Iio a)), Order.succ ((↑x).add b)) (⨆ (x : ↑(Set.Iio b)), Order.succ (a.add ↑x))

Instances For

instance NatOrdinal.instAdd :

Equations

NatOrdinal.instAdd = { add := NatOrdinal.add }

def NatOrdinal.«term_+ₒ_» :

Lean.TrailingParserDescr

Add two NatOrdinals as ordinal numbers.

Equations

NatOrdinal.«term_+ₒ_» = Lean.ParserDescr.trailingNode `NatOrdinal.«term_+ₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+ₒ") (Lean.ParserDescr.cat `term 66))

Instances For

theorem NatOrdinal.add_def (a b : NatOrdinal) :

a + b = max (⨆ (x : ↑(Set.Iio a)), Order.succ (↑x + b)) (⨆ (x : ↑(Set.Iio b)), Order.succ (a + ↑x))

theorem NatOrdinal.lt_add_iff {a b c : NatOrdinal} :

a < b + c ↔ (∃ b' < b, a ≤ b' + c) ∨ ∃ c' < c, a ≤ b + c'

theorem NatOrdinal.add_le_iff {a b c : NatOrdinal} :

b + c ≤ a ↔ (∀ b' < b, b' + c < a) ∧ ∀ c' < c, b + c' < a

instance NatOrdinal.instAddLeftStrictMono :

AddLeftStrictMono NatOrdinal

instance NatOrdinal.instAddRightStrictMono :

AddRightStrictMono NatOrdinal

instance NatOrdinal.instAddLeftMono :

AddLeftMono NatOrdinal

instance NatOrdinal.instAddRightMono :

AddRightMono NatOrdinal

instance NatOrdinal.instAddCommMonoid :

AddCommMonoid NatOrdinal

Equations

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

instance NatOrdinal.instIsOrderedCancelAddMonoid :

IsOrderedCancelAddMonoid NatOrdinal

theorem NatOrdinal.le_add_left {a b : NatOrdinal} :

a ≤ b + a

theorem NatOrdinal.le_add_right {a b : NatOrdinal} :

a ≤ a + b

instance NatOrdinal.instSuccAddOrder :

SuccAddOrder NatOrdinal

Equations

NatOrdinal.instSuccAddOrder = { toSuccOrder := NatOrdinal.instSuccOrder, succ_eq_add_one := NatOrdinal.succ_eq_add_one'✝ }

@[simp]

theorem NatOrdinal.of_add_one (a : Ordinal.{u_1}) :

of (a + 1) = of a + 1

@[simp]

theorem NatOrdinal.val_add_one (a : NatOrdinal) :

val (a + 1) = val a + 1

@[simp]

theorem NatOrdinal.add_one_ne_zero (a : NatOrdinal) :

a + 1 ≠ 0

instance NatOrdinal.instAddMonoidWithOne :

AddMonoidWithOne NatOrdinal

Equations

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

@[simp]

theorem NatOrdinal.of_natCast (n : ℕ) :

of ↑n = ↑n

@[simp]

theorem NatOrdinal.val_natCast (n : ℕ) :

val ↑n = ↑n

@[simp]

theorem NatOrdinal.succ_one :

Order.succ 1 = 2

@[simp]

theorem NatOrdinal.natCast_image_Iio' (n : ℕ) :

Nat.cast '' Set.Iio n = Set.Iio ↑n

@[simp]

theorem NatOrdinal.natCast_image_Iio (n : ℕ) :

Nat.cast '' Set.Iio n = Set.Iio ↑n

@[simp]

theorem NatOrdinal.forall_lt_natCast {P : NatOrdinal → Prop} {n : ℕ} :

(∀ a < ↑n, P a) ↔ ∀ a < n, P ↑a

@[simp]

theorem NatOrdinal.exists_lt_natCast {P : NatOrdinal → Prop} {n : ℕ} :

(∃ a < ↑n, P a) ↔ ∃ a < n, P ↑a

instance NatOrdinal.instCharZero :

CharZero NatOrdinal

@[simp]

theorem NatOrdinal.of_add_natCast (a : Ordinal.{u_1}) (n : ℕ) :

of (a + ↑n) = of a + ↑n

@[simp]

theorem NatOrdinal.val_add_natCast (a : NatOrdinal) (n : ℕ) :

val (a + ↑n) = val a + ↑n

theorem NatOrdinal.oadd_le_add' (a b : Ordinal.{u_1}) :

a + b ≤ val (of a + of b)

A version of oadd_le_add stated in terms of Ordinal.

theorem NatOrdinal.oadd_le_add (a b : NatOrdinal) :

of (val a + val b) ≤ a + b

Natural multiplication #

@[irreducible]

noncomputable def NatOrdinal.mul (a b : NatOrdinal) :

Natural multiplication on ordinals a * b, also known as the Hessenberg product, is recursively defined as the least ordinal such that a * b + a' * b' is greater than a' * b + a * b' for all a' < a and b < b'. In contrast to normal ordinal multiplication, it is commutative and distributive (over natural addition).

Natural multiplication can equivalently be characterized as the ordinal resulting from multiplying the Cantor normal forms of a and b as if they were polynomials in ω. Addition of exponents is done via natural addition.

Equations

a.mul b = sInf {c : NatOrdinal | ∀ a' < a, ∀ b' < b, a'.mul b + a.mul b' < c + a'.mul b'}

Instances For

instance NatOrdinal.instMul :

Equations

NatOrdinal.instMul = { mul := NatOrdinal.mul }

def NatOrdinal.«term_*ₒ_» :

Lean.TrailingParserDescr

Multiply two NatOrdinals as ordinal numbers.

Equations

NatOrdinal.«term_*ₒ_» = Lean.ParserDescr.trailingNode `NatOrdinal.«term_*ₒ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*ₒ") (Lean.ParserDescr.cat `term 71))

Instances For

theorem NatOrdinal.mul_def (a b : NatOrdinal) :

a * b = sInf {c : NatOrdinal | ∀ a' < a, ∀ b' < b, a' * b + a * b' < c + a' * b'}

theorem NatOrdinal.mul_add_lt {a b a' b' : NatOrdinal} (ha : a' < a) (hb : b' < b) :

a' * b + a * b' < a * b + a' * b'

theorem NatOrdinal.mul_add_le {a b a' b' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) :

a' * b + a * b' ≤ a * b + a' * b'

theorem NatOrdinal.lt_mul_iff {a b c : NatOrdinal} :

c < a * b ↔ ∃ a' < a, ∃ b' < b, c + a' * b' ≤ a' * b + a * b'

theorem NatOrdinal.mul_le_iff {a b c : NatOrdinal} :

a * b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' * b + a * b' < c + a' * b'

instance NatOrdinal.instCommMagma :

CommMagma NatOrdinal

Equations

NatOrdinal.instCommMagma = { toMul := NatOrdinal.instMul, mul_comm := NatOrdinal.mul_comm'✝ }

instance NatOrdinal.instMulZeroClass :

MulZeroClass NatOrdinal

Equations

NatOrdinal.instMulZeroClass = { toMul := NatOrdinal.instMul, toZero := instNatOrdinalZero, zero_mul := NatOrdinal.instMulZeroClass._proof_1, mul_zero := NatOrdinal.mul_zero'✝ }

instance NatOrdinal.instMulZeroOneClass :

MulZeroOneClass NatOrdinal

Equations

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

instance NatOrdinal.instPosMulStrictMono :

PosMulStrictMono NatOrdinal

instance NatOrdinal.instMulPosStrictMono :

MulPosStrictMono NatOrdinal

instance NatOrdinal.instMulLeftMono :

MulLeftMono NatOrdinal

instance NatOrdinal.instMulRightMono :

MulRightMono NatOrdinal

instance NatOrdinal.instDistrib :

Distrib NatOrdinal

Equations

NatOrdinal.instDistrib = { toMul := NatOrdinal.instMul, toAdd := NatOrdinal.instAdd, left_distrib := NatOrdinal.mul_add✝, right_distrib := NatOrdinal.instDistrib._proof_1 }

theorem NatOrdinal.mul_add_lt₃ {a b c a' b' c' : NatOrdinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) :

a' * b * c + a * b' * c + a * b * c' + a' * b' * c' < a * b * c + a' * b' * c + a' * b * c' + a * b' * c'

theorem NatOrdinal.mul_add_le₃ {a b c a' b' c' : NatOrdinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) :

a' * b * c + a * b' * c + a * b * c' + a' * b' * c' ≤ a * b * c + a' * b' * c + a' * b * c' + a * b' * c'

theorem NatOrdinal.lt_mul_iff₃ {a b c d : NatOrdinal} :

d < a * b * c ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, d + a' * b' * c + a' * b * c' + a * b' * c' ≤ a' * b * c + a * b' * c + a * b * c' + a' * b' * c'

theorem NatOrdinal.mul_le_iff₃ {a b c d : NatOrdinal} :

a * b * c ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c, a' * b * c + a * b' * c + a * b * c' + a' * b' * c' < d + a' * b' * c + a' * b * c' + a * b' * c'

instance NatOrdinal.instCommSemiring :

CommSemiring NatOrdinal

Equations

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

instance NatOrdinal.instIsStrictOrderedRing :

IsStrictOrderedRing NatOrdinal

theorem NatOrdinal.omul_le_mul' (a b : Ordinal.{u_1}) :

a * b ≤ val (of a * of b)

A version of omul_le_mul stated in terms of Ordinal.

theorem NatOrdinal.omul_le_mul (a b : NatOrdinal) :

of (val a * val b) ≤ a * b