Cantor Normal Form

The Cantor normal form of an ordinal is generally defined as its base ω expansion, with its non-zero exponents in decreasing order. Here, we more generally define a base b expansion Ordinal.CNF in this manner, which is well-behaved for any b ≥ 2.

Implementation notes

We implement Ordinal.CNF as an association list, where keys are exponents and values are coefficients. This is because this structure intrinsically reflects two key properties of the Cantor normal form:

• It is ordered.
• It has finitely many entries.

Todo

• Add API for the coefficients of the Cantor normal form.
• Prove the basic results relating the CNF to the arithmetic operations on ordinals.

@[irreducible]

noncomputable def Ordinal.CNFRec (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) (o : Ordinal.{u_2}) : C o

Inducts on the base b expansion of an ordinal.

Equations

• b.CNFRec H0 H o = if h : o = 0 then ⋯ ▸ H0 else H o h (b.CNFRec H0 H (o % b ^ Ordinal.log b o))

@[simp]

theorem Ordinal.CNFRec_zero {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : b.CNFRec H0 H 0 = H0

theorem Ordinal.CNFRec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) : b.CNFRec H0 H o = H o ho (b.CNFRec H0 H (o % b ^ log b o))

def Ordinal.CNF (b o : Ordinal.{u_1}) : List (Ordinal.{u_1} × Ordinal.{u_1})

The Cantor normal form of an ordinal o is the list of coefficients and exponents in the base-b expansion of o.

We special-case CNF 0 o = CNF 1 o = [(0, o)] for o ≠ 0.

CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

Equations

• Ordinal.CNF b o = b.CNFRec [] (fun (o : Ordinal.{?u.14}) (x : o ≠ 0) (IH : List (Ordinal.{?u.14} × Ordinal.{?u.14})) => (Ordinal.log b o, o / b ^ Ordinal.log b o) :: IH) o

@[simp]

theorem Ordinal.CNF_zero (b : Ordinal.{u_1}) : CNF b 0 = []

theorem Ordinal.CNF_ne_zero {b o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Recursive definition for the Cantor normal form.

theorem Ordinal.zero_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 0 o = [(0, o)]

theorem Ordinal.one_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) : CNF 1 o = [(0, o)]

theorem Ordinal.CNF_of_le_one {b o : Ordinal.{u_1}} (hb : b ≤ 1) (ho : o ≠ 0) : CNF b o = [(0, o)]

theorem Ordinal.CNF_of_lt {b o : Ordinal.{u_1}} (ho : o ≠ 0) (hb : o < b) : CNF b o = [(0, o)]

theorem Ordinal.CNF_foldr (b o : Ordinal.{u_1}) : List.foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Evaluating the Cantor normal form of an ordinal returns the ordinal.

theorem Ordinal.CNF_fst_le_log {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.1 ≤ log b o

Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

theorem Ordinal.CNF_lt_snd {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → 0 < x.2

Every coefficient in a Cantor normal form is positive.

theorem Ordinal.CNF_snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} : x ∈ CNF b o → x.2 < b

Every coefficient in the Cantor normal form CNF b o is less than b.

theorem Ordinal.CNF_sorted (b o : Ordinal.{u_1}) : List.Sorted (fun (x1 x2 : Ordinal.{u_1}) => x1 > x2) (List.map Prod.fst (CNF b o))

The exponents of the Cantor normal form are decreasing.