mathlib3 documentation

set_theory.ordinal.cantor_normal_form

Cantor Normal Form #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable def ordinal.CNF_rec (b : ordinal) {C : ordinal → Sort u_2} (H0 : C 0) (H : Π (o : ordinal), o ≠ 0 → C (o % b ^ ordinal.log b o) → C o) (o : ordinal) :

C o

Inducts on the base b expansion of an ordinal.

Equations

b.CNF_rec H0 H o = dite (o = 0) (λ (ho : o = 0), _.mpr H0) (λ (ho : ¬o = 0), let hwf : o % b ^ ordinal.log b o < o := _ in H o ho (b.CNF_rec H0 H (o % b ^ ordinal.log b o)))

@[simp]

theorem ordinal.CNF_rec_zero {C : ordinal → Sort u_2} (b : ordinal) (H0 : C 0) (H : Π (o : ordinal), o ≠ 0 → C (o % b ^ ordinal.log b o) → C o) :

b.CNF_rec H0 H 0 = H0

theorem ordinal.CNF_rec_pos (b : ordinal) {o : ordinal} {C : ordinal → Sort u_2} (ho : o ≠ 0) (H0 : C 0) (H : Π (o : ordinal), o ≠ 0 → C (o % b ^ ordinal.log b o) → C o) :

b.CNF_rec H0 H o = H o ho (b.CNF_rec H0 H (o % b ^ ordinal.log b o))

noncomputable def ordinal.CNF (b o : ordinal) :

list (ordinal × ordinal)

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.CNF_rec list.nil (λ (o : ordinal) (ho : o ≠ 0) (IH : list (ordinal × ordinal)), (ordinal.log b o, o / b ^ ordinal.log b o) :: IH) o

@[simp]

theorem ordinal.CNF_zero (b : ordinal) :

ordinal.CNF b 0 = list.nil

theorem ordinal.CNF_ne_zero {b o : ordinal} (ho : o ≠ 0) :

ordinal.CNF b o = (ordinal.log b o, o / b ^ ordinal.log b o) :: ordinal.CNF b (o % b ^ ordinal.log b o)

Recursive definition for the Cantor normal form.

theorem ordinal.zero_CNF {o : ordinal} (ho : o ≠ 0) :

ordinal.CNF 0 o = [(0, o)]

theorem ordinal.one_CNF {o : ordinal} (ho : o ≠ 0) :

ordinal.CNF 1 o = [(0, o)]

theorem ordinal.CNF_of_le_one {b o : ordinal} (hb : b ≤ 1) (ho : o ≠ 0) :

ordinal.CNF b o = [(0, o)]

theorem ordinal.CNF_of_lt {b o : ordinal} (ho : o ≠ 0) (hb : o < b) :

ordinal.CNF b o = [(0, o)]

theorem ordinal.CNF_foldr (b o : ordinal) :

list.foldr (λ (p : ordinal × ordinal) (r : ordinal), b ^ p.fst * p.snd + r) 0 (ordinal.CNF b o) = o

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

theorem ordinal.CNF_fst_le_log {b o : ordinal} {x : ordinal × ordinal} :

x ∈ ordinal.CNF b o → x.fst ≤ ordinal.log b o

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

theorem ordinal.CNF_fst_le {b o : ordinal} {x : ordinal × ordinal} (h : x ∈ ordinal.CNF b o) :

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

theorem ordinal.CNF_lt_snd {b o : ordinal} {x : ordinal × ordinal} :

x ∈ ordinal.CNF b o → 0 < x.snd

Every coefficient in a Cantor normal form is positive.

theorem ordinal.CNF_snd_lt {b o : ordinal} (hb : 1 < b) {x : ordinal × ordinal} :

x ∈ ordinal.CNF b o → x.snd < b

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

theorem ordinal.CNF_sorted (b o : ordinal) :

list.sorted gt (list.map prod.fst (ordinal.CNF b o))

The exponents of the Cantor normal form are decreasing.