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.opow_le_one {x : Ordinal.{u_1}} (hx : x ≤ 1) (y : Ordinal.{u_1}) :

x ^ y ≤ 1

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

@[instance_reducible]

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) :

@[simp]

theorem NatOrdinal.wpow_one :

ω^ 1 = of Ordinal.omega0

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.of_omega0_opow_mul_natCast_add' {x y : Ordinal.{u_1}} (hy : y < Ordinal.omega0 ^ x) (n : ℕ) :

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

See of_omega0_opow_mul_natCast_add for a stronger version.

theorem NatOrdinal.of_omega0_opow_add' {x y : Ordinal.{u_1}} (hy : y < Ordinal.omega0 ^ x) :

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

See of_omega0_opow_add for a stronger version.

@[simp]

theorem NatOrdinal.of_omega0_opow_mul_natCast (x : Ordinal.{u_1}) (n : ℕ) :

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

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

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

theorem NatOrdinal.wpow_mul_natCast_lt {x y : NatOrdinal} (h : x < y) (n : ℕ) :

ω^ x * ↑n < ω^ y

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.of_omega0_opow_mul_natCast_add {x y : Ordinal.{u_1}} (hy : y < Ordinal.omega0 ^ (x + 1)) (n : ℕ) :

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

theorem NatOrdinal.of_omega0_opow_add {x y : Ordinal.{u_1}} (hy : y < Ordinal.omega0 ^ (x + 1)) :

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

theorem NatOrdinal.of_omega0_opow_add_omega0_opow {x y : Ordinal.{u_1}} (h : x ≤ y) :

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

theorem NatOrdinal.of_natCast_opow_mul_natCast_add_of_lt {x y : Ordinal.{u_1}} {m : ℕ} (hy : y < ↑m ^ x * Ordinal.omega0) (n : ℕ) :

of (↑m ^ x * ↑n + y) = of (↑m ^ x) * ↑n + of y

theorem NatOrdinal.of_natCast_opow_mul_natCast_add_of_lt' {x y : Ordinal.{u_1}} {m : ℕ} (hy : y < ↑m ^ x) (n : ℕ) :

of (↑m ^ x * ↑n + y) = of (↑m ^ x) * ↑n + of y

See of_natCast_opow_mul_natCast_add_of_lt for a stronger version.

theorem NatOrdinal.of_natCast_opow_add_of_lt {x y : Ordinal.{u_1}} {m : ℕ} (hy : y < ↑m ^ x * Ordinal.omega0) :

of (↑m ^ x + y) = of (↑m ^ x) + of y

theorem NatOrdinal.of_natCast_opow_add_of_lt' {x y : Ordinal.{u_1}} {m : ℕ} (hy : y < ↑m ^ x) :

of (↑m ^ x + y) = of (↑m ^ x) + of y

See of_natCast_opow_add_of_lt for a stronger version.

@[simp]

theorem NatOrdinal.of_natCast_opow_mul_natCast {x : Ordinal.{u_1}} (m n : ℕ) :

of (↑m ^ x * ↑n) = of (↑m ^ x) * ↑n

theorem NatOrdinal.wpow_add (x y : NatOrdinal) :

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

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

x * y < ω^ ω^ z