Documentation

CombinatorialGames.NatOrdinal.Pow

Natural operations on `ω ^ x` #

This file characterizes natural operations on powers of ω. In particular, we show:

If y < ω^ x, then ω^ x * n + y = of (ω ^ x.val * n + y.val).
ω^ (x + y) = ω^ x * ω^ y.

These two results imply the validity of an algorithm to evaluate natural addition and multiplication: write down the base ω Cantor Normal Forms of both ordinals, and add/multiply them as polynomials.

Implementation notes #

Surreal exponentiation is not closed on the ordinals. Because of this, we opt against defining a Pow instance on NatOrdinal. Instead, we implement our own custom typeclass Wpow, giving us notation ω^ x for of (ω ^ x.val). This typeclass will get reused for IGame and Surreal in CombinatorialGames.Surreal.Pow.

theorem Ordinal.lt_mul_add_one {x y z : Ordinal.{u_1}} :

x < y * (z + 1) ↔ ∃ w < y, x ≤ y * z + w

class Wpow (α : Type u_1) :

Type u_1

A typeclass for the the ω^ notation.

wpow : α → α
The ω-map, i.e. base ω exponentiation.

Instances

def «termω^_» :

Lean.ParserDescr

The ω-map, i.e. base ω exponentiation.

Conventions for notations in identifiers:

The recommended spelling of ω^ in identifiers is wpow.

Equations

«termω^_» = Lean.ParserDescr.node `«termω^_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ω^ ") (Lean.ParserDescr.cat `term 75))

Instances For

noncomputable instance NatOrdinal.instWpow :

Wpow NatOrdinal

Equations

NatOrdinal.instWpow = { wpow := fun (x : NatOrdinal) => NatOrdinal.of (Ordinal.omega0 ^ NatOrdinal.val x) }

theorem NatOrdinal.wpow_def (x : NatOrdinal) :

ω^ x = of (Ordinal.omega0 ^ val x)

@[simp]

theorem NatOrdinal.of_omega0_opow (x : Ordinal.{u_1}) :

of (Ordinal.omega0 ^ x) = ω^ of x

@[simp]

theorem NatOrdinal.val_wpow (x : NatOrdinal) :

val (ω^ x) = Ordinal.omega0 ^ val x

@[simp]

theorem NatOrdinal.wpow_zero :

ω^ 0 = 1

@[simp]

theorem NatOrdinal.wpow_pos (x : NatOrdinal) :

0 < ω^ x

@[simp]

theorem NatOrdinal.wpow_ne_zero (x : NatOrdinal) :

theorem NatOrdinal.isNormal_wpow :

Order.IsNormal fun (x : NatOrdinal) => ω^ x

@[simp]

theorem NatOrdinal.wpow_lt_wpow {x y : NatOrdinal} :

ω^ x < ω^ y ↔ x < y

@[simp]

theorem NatOrdinal.wpow_le_wpow {x y : NatOrdinal} :

ω^ x ≤ ω^ y ↔ x ≤ y

@[simp]

theorem NatOrdinal.wpow_inj {x y : NatOrdinal} :

ω^ x = ω^ y ↔ x = y

theorem NatOrdinal.add_lt_wpow {x y z : NatOrdinal} (hx : x < ω^ z) (hy : y < ω^ z) :

x + y < ω^ z

theorem NatOrdinal.wpow_mul_natCast_add_of_lt' {x y : NatOrdinal} (hy : y < ω^ x) (n : ℕ) :

ω^ x * ↑n + y = of (Ordinal.omega0 ^ val x * ↑n + val y)

See wpow_mul_natCast_add_of_lt for a stronger version.

theorem NatOrdinal.wpow_add_of_lt' {x y : NatOrdinal} (hy : y < ω^ x) :

ω^ x + y = of (Ordinal.omega0 ^ val x + val y)

See wpow_add_of_lt for a stronger version.

theorem NatOrdinal.wpow_mul_natCast (x : NatOrdinal) (n : ℕ) :

ω^ x * ↑n = of (Ordinal.omega0 ^ val x * ↑n)

theorem NatOrdinal.wpow_mul_natCast_lt {a b : NatOrdinal} (h : a < b) (n : ℕ) :

ω^ a * ↑n < ω^ b

theorem NatOrdinal.lt_wpow_iff {x y : NatOrdinal} (hx : x ≠ 0) :

y < ω^ x ↔ ∃ z < x, ∃ (n : ℕ), y < ω^ z * ↑n

theorem NatOrdinal.wpow_le_iff {x y : NatOrdinal} (hx : x ≠ 0) :

ω^ x ≤ y ↔ ∀ z < x, ∀ (n : ℕ), ω^ z * ↑n ≤ y

theorem NatOrdinal.lt_wpow_add_one_iff {x y : NatOrdinal} :

y < ω^ (x + 1) ↔ ∃ (n : ℕ), y < ω^ x * ↑n

theorem NatOrdinal.wpow_add_one_le_iff {x y : NatOrdinal} :

ω^ (x + 1) ≤ y ↔ ∀ (n : ℕ), ω^ x * ↑n ≤ y

theorem NatOrdinal.wpow_mul_natCast_add_of_lt {x y : NatOrdinal} (hy : y < ω^ (x + 1)) (n : ℕ) :

ω^ x * ↑n + y = of (Ordinal.omega0 ^ val x * ↑n + val y)

theorem NatOrdinal.wpow_add_of_lt {x y : NatOrdinal} (hy : y < ω^ (x + 1)) :

ω^ x + y = of (Ordinal.omega0 ^ val x + val y)

theorem NatOrdinal.wpow_add_wpow {x y : NatOrdinal} (h : x ≤ y) :

ω^ y + ω^ x = of (Ordinal.omega0 ^ val y + Ordinal.omega0 ^ val x)

@[irreducible]

theorem NatOrdinal.wpow_add (x y : NatOrdinal) :

ω^ (x + y) = ω^ x * ω^ y