# mathlib3documentation

set_theory.ordinal.notation

# Ordinal notation #

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

Constructive ordinal arithmetic for ordinals below ε₀.

We define a type onote, with constructors 0 : onote and onote.oadd e n a representing ω ^ e * n + a. We say that o is in Cantor normal form - onote.NF o - if either o = 0 or o = ω ^ e * n + a with a < ω ^ e and a in Cantor normal form.

The type nonote is the type of ordinals below ε₀ in Cantor normal form. Various operations (addition, subtraction, multiplication, power function) are defined on onote and nonote.

inductive onote  :

Recursive definition of an ordinal notation. zero denotes the ordinal 0, and oadd e n a is intended to refer to ω^e * n + a. For this to be valid Cantor normal form, we must have the exponents decrease to the right, but we can't state this condition until we've defined repr, so it is a separate definition NF.

Instances for onote
@[protected, instance]
@[protected, instance]

Notation for 0

Equations
@[simp]
theorem onote.zero_def  :
@[protected, instance]
Equations
@[protected, instance]

Notation for 1

Equations
def onote.omega  :

Notation for ω

Equations
@[simp]
noncomputable def onote.repr  :

The ordinal denoted by a notation

Equations
def onote.to_string_aux1 (e : onote) (n : ) (s : string) :

Auxiliary definition to print an ordinal notation

Equations

Print an ordinal notation

Equations
def onote.repr'  :

Print an ordinal notation

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem onote.lt_def {x y : onote} :
x < y x.repr < y.repr
theorem onote.le_def {x y : onote} :
x y x.repr y.repr
@[simp]
def onote.of_nat  :

Convert a nat into an ordinal

Equations
Instances for onote.of_nat
@[simp]
theorem onote.of_nat_one  :
@[simp]
theorem onote.repr_of_nat (n : ) :
@[simp]
theorem onote.repr_one  :
1.repr = 1
theorem onote.omega_le_oadd (e : onote) (n : ℕ+) (a : onote) :
theorem onote.oadd_pos (e : onote) (n : ℕ+) (a : onote) :
def onote.cmp  :

Compare ordinal notations

Equations
theorem onote.eq_of_cmp_eq {o₁ o₂ : onote} :
o₁.cmp o₂ = ordering.eq o₁ = o₂
@[protected]
theorem onote.zero_lt_one  :
0 < 1
inductive onote.NF_below  :

NF_below o b says that o is a normal form ordinal notation satisfying repr o < ω ^ b.

@[class]
structure onote.NF (o : onote) :
Prop
• out :

A normal form ordinal notation has the form

ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ


where a₁ > a₂ > ... > aₖ and all the aᵢ are also in normal form.

We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

Instances of this typeclass
Instances of other typeclasses for onote.NF
@[protected, instance]
def onote.NF.zero  :
theorem onote.NF_below.oadd {e : onote} {n : ℕ+} {a : onote} {b : ordinal} :
a.NF_below e.repr e.repr < b (e.oadd n a).NF_below b
theorem onote.NF_below.fst {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :
theorem onote.NF.fst {e : onote} {n : ℕ+} {a : onote} :
theorem onote.NF_below.snd {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :
theorem onote.NF.snd' {e : onote} {n : ℕ+} {a : onote} :
theorem onote.NF.snd {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) :
theorem onote.NF.oadd {e a : onote} (h₁ : onote.NF e) (n : ℕ+) (h₂ : a.NF_below e.repr) :
@[protected, instance]
def onote.NF.oadd_zero (e : onote) (n : ℕ+) [h : onote.NF e] :
theorem onote.NF_below.lt {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (h : (e.oadd n a).NF_below b) :
e.repr < b
theorem onote.NF_below_zero {o : onote} :
o.NF_below 0 o = 0
theorem onote.NF.zero_of_zero {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) (e0 : e = 0) :
a = 0
theorem onote.NF_below.repr_lt {o : onote} {b : ordinal} (h : o.NF_below b) :
o.repr <
theorem onote.NF_below.mono {o : onote} {b₁ b₂ : ordinal} (bb : b₁ b₂) (h : o.NF_below b₁) :
o.NF_below b₂
theorem onote.NF.below_of_lt {e : onote} {n : ℕ+} {a : onote} {b : ordinal} (H : e.repr < b) :
theorem onote.NF.below_of_lt' {o : onote} {b : ordinal} :
@[protected, instance]
def onote.NF_of_nat (n : ) :
@[protected, instance]
def onote.NF_one  :
theorem onote.oadd_lt_oadd_1 {e₁ : onote} {n₁ : ℕ+} {o₁ e₂ : onote} {n₂ : ℕ+} {o₂ : onote} (h₁ : onote.NF (e₁.oadd n₁ o₁)) (h : e₁ < e₂) :
theorem onote.oadd_lt_oadd_2 {e o₁ o₂ : onote} {n₁ n₂ : ℕ+} (h₁ : onote.NF (e.oadd n₁ o₁)) (h : n₁ < n₂) :
theorem onote.oadd_lt_oadd_3 {e : onote} {n : ℕ+} {a₁ a₂ : onote} (h : a₁ < a₂) :
theorem onote.cmp_compares (a b : onote) [onote.NF a] [onote.NF b] :
(a.cmp b).compares a b
theorem onote.repr_inj {a b : onote} [onote.NF a] [onote.NF b] :
a.repr = b.repr a = b
theorem onote.NF.of_dvd_omega_opow {b : ordinal} {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) (d : (e.oadd n a).repr) :
theorem onote.NF.of_dvd_omega {e : onote} {n : ℕ+} {a : onote} (h : onote.NF (e.oadd n a)) :
def onote.top_below (b : onote) :
onote Prop

top_below b o asserts that the largest exponent in o, if it exists, is less than b. This is an auxiliary definition for decidability of NF.

Equations
Instances for onote.top_below
@[protected, instance]
Equations
@[protected, instance]
Equations

Addition of ordinal notations (correct only for normal input)

Equations
@[protected, instance]
Equations
@[simp]
theorem onote.zero_add (o : onote) :
0 + o = o
theorem onote.oadd_add (e : onote) (n : ℕ+) (a o : onote) :
e.oadd n a + o = onote.add._match_1 e n (a + o)
def onote.sub  :

Subtraction of ordinal notations (correct only for normal input)

Equations
• (e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂) = onote.sub._match_1 e₁ n₁ a₁ n₂ (a₁.sub a₂) (e₁.cmp e₂)
• 0.sub (ᾰ.oadd ᾰ_1 ᾰ_2) = 0
• = 0
• onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.gt = e₁.oadd n₁ a₁
• onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.eq = onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 (n₁ - n₂)
• onote.sub._match_1 e₁ n₁ a₁ n₂ _f_1 ordering.lt = 0
• onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 k.succ = e₁.oadd k.succ_pnat a₁
• onote.sub._match_2 e₁ n₁ a₁ n₂ _f_1 0 = ite (n₁ = n₂) _f_1 0
@[protected, instance]
Equations
theorem onote.add_NF_below {b : ordinal} {o₁ o₂ : onote} :
o₁.NF_below b o₂.NF_below b (o₁ + o₂).NF_below b
@[protected, instance]
def onote.add_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
onote.NF (o₁ + o₂)
@[simp]
theorem onote.repr_add (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
(o₁ + o₂).repr = o₁.repr + o₂.repr
theorem onote.sub_NF_below {o₁ o₂ : onote} {b : ordinal} :
o₁.NF_below b onote.NF o₂ (o₁ - o₂).NF_below b
@[protected, instance]
def onote.sub_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
onote.NF (o₁ - o₂)
@[simp]
theorem onote.repr_sub (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
(o₁ - o₂).repr = o₁.repr - o₂.repr
def onote.mul  :

Multiplication of ordinal notations (correct only for normal input)

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem onote.oadd_mul (e₁ : onote) (n₁ : ℕ+) (a₁ e₂ : onote) (n₂ : ℕ+) (a₂ : onote) :
theorem onote.oadd_mul_NF_below {e₁ : onote} {n₁ : ℕ+} {a₁ : onote} {b₁ : ordinal} (h₁ : (e₁.oadd n₁ a₁).NF_below b₁) {o₂ : onote} {b₂ : ordinal} :
o₂.NF_below b₂ (e₁.oadd n₁ a₁ * o₂).NF_below (e₁.repr + b₂)
@[protected, instance]
def onote.mul_NF (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
onote.NF (o₁ * o₂)
@[simp]
theorem onote.repr_mul (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
(o₁ * o₂).repr = o₁.repr * o₂.repr
def onote.split'  :

Calculate division and remainder of o mod ω. split' o = (a, n) means o = ω * a + n.

Equations
def onote.split  :

Calculate division and remainder of o mod ω. split o = (a, n) means o = a + n, where ω ∣ a.

Equations
def onote.scale (x : onote) :

scale x o is the ordinal notation for ω ^ x * o.

Equations
Instances for onote.scale
def onote.mul_nat  :

mul_nat o n is the ordinal notation for o * n.

Equations
Instances for onote.mul_nat
def onote.opow_aux (e a0 a : onote) :

Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

Equations
Instances for onote.opow_aux
def onote.opow (o₁ o₂ : onote) :

opow o₁ o₂ calculates the ordinal notation for the ordinal exponential o₁ ^ o₂.

Equations
• o₁.opow o₂ = onote.opow._match_1 o₂ o₁.split
• onote.opow._match_1 o₂ (a0.oadd _x _x_1, m) = onote.opow._match_3 a0 _x _x_1 m o₂.split
• onote.opow._match_1 o₂ (0, m + 1) = onote.opow._match_2 m o₂.split'
• onote.opow._match_1 o₂ (0, 1) = 1
• onote.opow._match_1 o₂ (0, 0) = ite (o₂ = 0) 1 0
• onote.opow._match_3 a0 _x _x_1 m (b, k + 1) = let eb : onote := a0 * b in (eb + a0.mul_nat k).scale (a0.oadd _x _x_1) + eb.opow_aux a0 ((a0.oadd _x _x_1).mul_nat m) k m
• onote.opow._match_3 a0 _x _x_1 m (b, 0) = (a0 * b).oadd 1 0
• onote.opow._match_2 m (b', k) = b'.oadd (m.succ_pnat ^ k) 0
@[protected, instance]
Equations
theorem onote.opow_def (o₁ o₂ : onote) :
o₁ ^ o₂ = onote.opow._match_1 o₂ o₁.split
theorem onote.split_eq_scale_split' {o o' : onote} {m : } [onote.NF o] :
o.split' = (o', m) o.split = (1.scale o', m)
theorem onote.NF_repr_split' {o o' : onote} {m : } [onote.NF o] :
o.split' = (o', m) onote.NF o' o.repr = + m
theorem onote.scale_eq_mul (x : onote) [onote.NF x] (o : onote) [onote.NF o] :
x.scale o = x.oadd 1 0 * o
@[protected, instance]
def onote.NF_scale (x : onote) [onote.NF x] (o : onote) [onote.NF o] :
@[simp]
theorem onote.repr_scale (x : onote) [onote.NF x] (o : onote) [onote.NF o] :
(x.scale o).repr = * o.repr
theorem onote.NF_repr_split {o o' : onote} {m : } [onote.NF o] (h : o.split = (o', m)) :
theorem onote.split_dvd {o o' : onote} {m : } [onote.NF o] (h : o.split = (o', m)) :
theorem onote.split_add_lt {o e : onote} {n : ℕ+} {a : onote} {m : } [onote.NF o] (h : o.split = (e.oadd n a, m)) :
a.repr + m <
@[simp]
theorem onote.mul_nat_eq_mul (n : ) (o : onote) :
o.mul_nat n =
@[protected, instance]
def onote.NF_mul_nat (o : onote) [onote.NF o] (n : ) :
@[protected, instance]
def onote.NF_opow_aux (e a0 a : onote) [onote.NF e] [onote.NF a0] [onote.NF a] (k m : ) :
onote.NF (e.opow_aux a0 a k m)
@[protected, instance]
def onote.NF_opow (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
onote.NF (o₁ ^ o₂)
theorem onote.scale_opow_aux (e a0 a : onote) [onote.NF e] [onote.NF a0] [onote.NF a] (k m : ) :
(e.opow_aux a0 a k m).repr = * (0.opow_aux a0 a k m).repr
theorem onote.repr_opow_aux₁ {e a : onote} [Ne : onote.NF e] [Na : onote.NF a] {a' : ordinal} (e0 : e.repr 0) (h : a' < ) (aa : a.repr = a') (n : ℕ+) :
theorem onote.repr_opow_aux₂ {a0 a' : onote} [N0 : onote.NF a0] [Na' : onote.NF a'] (m : ) (d : ordinal.omega a'.repr) (e0 : a0.repr 0) (h : a'.repr + m < ) (n : ℕ+) (k : ) :
let R : ordinal := (0.opow_aux a0 (a0.oadd n a' * k m).repr in (k 0 R < (ordinal.omega ^ a0.repr) ^ (ordinal.omega ^ a0.repr) ^ k * * n + a'.repr) + R = * n + a'.repr + m) ^
theorem onote.repr_opow (o₁ o₂ : onote) [onote.NF o₁] [onote.NF o₂] :
(o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Given an ordinal, returns inl none for 0, inl (some a) for a+1, and inr f for a limit ordinal a, where f i is a sequence converging to a.

Equations

The property satisfied by fundamental_sequence o:

• inl none means o = 0
• inl (some a) means o = succ a
• inr f means o is a limit ordinal and f is a strictly increasing sequence which converges to o
Equations

The fast growing hierarchy for ordinal notations < ε₀. This is a sequence of functions ℕ → ℕ indexed by ordinals, with the definition:

• f_0(n) = n + 1
• f_(α+1)(n) = f_α^[n](n)
• f_α(n) = f_(α[n])(n) where α is a limit ordinal and α[i] is the fundamental sequence converging to α
Equations
theorem onote.fast_growing_def {o : onote} {x : ( onote)} (e : o.fundamental_sequence = x) :
o.fast_growing = onote.fast_growing._match_1 o (λ (a : onote) (_x : (_x : a < o), a.fast_growing) (λ (f : (_x : (i : ) (_x : f i < o), (f i).fast_growing i) x _
theorem onote.fast_growing_limit (o : onote) {f : onote} (h : o.fundamental_sequence = ) :
o.fast_growing = λ (i : ), (f i).fast_growing i
@[simp]
@[simp]
theorem onote.fast_growing_one  :
1.fast_growing = λ (n : ), 2 * n
@[simp]
theorem onote.fast_growing_two  :
2.fast_growing = λ (n : ), 2 ^ n * n

We can extend the fast growing hierarchy one more step to ε₀ itself, using ω^(ω^...^ω^0) as the fundamental sequence converging to ε₀ (which is not an onote). Extending the fast growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals.

Equations
def nonote  :

The type of normal ordinal notations. (It would have been nicer to define this right in the inductive type, but NF o requires repr which requires onote, so all these things would have to be defined at once, which messes up the VM representation.)

Equations
Instances for nonote
@[protected, instance]
Equations
@[protected, instance]
def nonote.NF (o : nonote) :
def nonote.mk (o : onote) [h : onote.NF o] :

Construct a nonote from an ordinal notation (and infer normality)

Equations
noncomputable def nonote.repr (o : nonote) :

The ordinal represented by an ordinal notation. (This function is noncomputable because ordinal arithmetic is noncomputable. In computational applications nonote can be used exclusively without reference to ordinal, but this function allows for correctness results to be stated.)

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem nonote.lt_wf  :
@[protected, instance]
@[protected, instance]
Equations
def nonote.of_nat (n : ) :

Convert a natural number to an ordinal notation

Equations
def nonote.cmp (a b : nonote) :

Compare ordinal notations

Equations
theorem nonote.cmp_compares (a b : nonote) :
(a.cmp b).compares a b
@[protected, instance]
Equations
@[protected, instance]
def nonote.below (a b : nonote) :
Prop

Asserts that repr a < ω ^ repr b. Used in nonote.rec_on

Equations
def nonote.oadd (e : nonote) (n : ℕ+) (a : nonote) (h : a.below e) :

The oadd pseudo-constructor for nonote

Equations
def nonote.rec_on {C : nonote Sort u_1} (o : nonote) (H0 : C 0) (H1 : Π (e : nonote) (n : ℕ+) (a : nonote) (h : a.below e), C e C a C (e.oadd n a h)) :
C o

This is a recursor-like theorem for nonote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

Equations
@[protected, instance]

Equations
theorem nonote.repr_add (a b : nonote) :
(a + b).repr = a.repr + b.repr
@[protected, instance]

Subtraction of ordinal notations

Equations
theorem nonote.repr_sub (a b : nonote) :
(a - b).repr = a.repr - b.repr
@[protected, instance]

Multiplication of ordinal notations

Equations
theorem nonote.repr_mul (a b : nonote) :
(a * b).repr = a.repr * b.repr
def nonote.opow (x y : nonote) :

Exponentiation of ordinal notations

Equations
theorem nonote.repr_opow (a b : nonote) :
(a.opow b).repr = a.repr ^ b.repr