# Documentation

Mathlib.SetTheory.Ordinal.Notation

# Ordinal notation #

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

Notation for 0

@[simp]
theorem ONote.zero_def :

Notation for 1

Notation for ω

Instances For
noncomputable def ONote.repr :

The ordinal denoted by a notation

Equations
Instances For
def ONote.toStringAux1 (e : ONote) (n : ) (s : String) :

Auxiliary definition to print an ordinal notation

Instances For

Print an ordinal notation

Equations
Instances For
def ONote.repr' (prec : ) :

Print an ordinal notation

Equations
• One or more equations did not get rendered due to their size.
• =
Instances For
theorem ONote.lt_def {x : ONote} {y : ONote} :
x < y
theorem ONote.le_def {x : ONote} {y : ONote} :
x y

Convert a Nat into an ordinal

Instances For
@[simp]
theorem ONote.ofNat_zero :
0 = 0
@[simp]
theorem ONote.ofNat_succ (n : ) :
↑() = ONote.oadd 0 () 0
instance ONote.nat (n : ) :
@[simp]
theorem ONote.ofNat_one :
1 = 1
@[simp]
theorem ONote.repr_ofNat (n : ) :
= n
theorem ONote.repr_one :
= 1
theorem ONote.omega_le_oadd (e : ONote) (n : ℕ+) (a : ONote) :
theorem ONote.oadd_pos (e : ONote) (n : ℕ+) (a : ONote) :
0 < ONote.oadd e n a
def ONote.cmp :

Compare ordinal notations

Equations
Instances For
theorem ONote.eq_of_cmp_eq {o₁ : ONote} {o₂ : ONote} :
ONote.cmp o₁ o₂ = Ordering.eqo₁ = o₂
inductive ONote.NFBelow :

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

Instances For
class ONote.NF (o : ONote) :
• 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
theorem ONote.NFBelow.oadd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} :
< bONote.NFBelow (ONote.oadd e n a) b
theorem ONote.NFBelow.fst {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) :
theorem ONote.NF.fst {e : ONote} {n : ℕ+} {a : ONote} :
theorem ONote.NFBelow.snd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) :
theorem ONote.NF.snd' {e : ONote} {n : ℕ+} {a : ONote} :
theorem ONote.NF.snd {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) :
theorem ONote.NF.oadd {e : ONote} {a : ONote} (h₁ : ) (n : ℕ+) (h₂ : ) :
instance ONote.NF.oadd_zero (e : ONote) (n : ℕ+) [h : ] :
theorem ONote.NFBelow.lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : ONote.NFBelow (ONote.oadd e n a) b) :
< b
theorem ONote.NFBelow_zero {o : ONote} :
o = 0
theorem ONote.NF.zero_of_zero {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) (e0 : e = 0) :
a = 0
theorem ONote.NFBelow.repr_lt {o : ONote} {b : Ordinal.{0}} (h : ) :
theorem ONote.NFBelow.mono {o : ONote} {b₁ : Ordinal.{0}} {b₂ : Ordinal.{0}} (bb : b₁ b₂) (h : ) :
theorem ONote.NF.below_of_lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (H : < b) :
theorem ONote.NF.below_of_lt' {o : ONote} {b : Ordinal.{0}} :
instance ONote.nf_ofNat (n : ) :
theorem ONote.oadd_lt_oadd_1 {e₁ : ONote} {n₁ : ℕ+} {o₁ : ONote} {e₂ : ONote} {n₂ : ℕ+} {o₂ : ONote} (h₁ : ONote.NF (ONote.oadd e₁ n₁ o₁)) (h : e₁ < e₂) :
theorem ONote.oadd_lt_oadd_2 {e : ONote} {o₁ : ONote} {o₂ : ONote} {n₁ : ℕ+} {n₂ : ℕ+} (h₁ : ONote.NF (ONote.oadd e n₁ o₁)) (h : n₁ < n₂) :
theorem ONote.oadd_lt_oadd_3 {e : ONote} {n : ℕ+} {a₁ : ONote} {a₂ : ONote} (h : a₁ < a₂) :
theorem ONote.cmp_compares (a : ONote) (b : ONote) [] [] :
theorem ONote.repr_inj {a : ONote} {b : ONote} [] [] :
a = b
theorem ONote.NF.of_dvd_omega_opow {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote} (h : ONote.NF (ONote.oadd e n a)) (d : ONote.repr (ONote.oadd e n a)) :
b
def ONote.TopBelow (b : ONote) :

TopBelow 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.

Instances For
Equations
• One or more equations did not get rendered due to their size.
def ONote.addAux (e : ONote) (n : ℕ+) (o : ONote) :

Auxiliary definition for add

Instances For

Addition of ordinal notations (correct only for normal input)

Equations
Instances For
@[simp]
theorem ONote.zero_add (o : ONote) :
0 + o = o
theorem ONote.oadd_add (e : ONote) (n : ℕ+) (a : ONote) (o : ONote) :
ONote.oadd e n a + o = ONote.addAux e n (a + o)
def ONote.sub :

Subtraction of ordinal notations (correct only for normal input)

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ONote.add_nfBelow {b : Ordinal.{0}} {o₁ : ONote} {o₂ : ONote} :
ONote.NFBelow (o₁ + o₂) b
instance ONote.add_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.NF (o₁ + o₂)
@[simp]
theorem ONote.repr_add (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.repr (o₁ + o₂) = +
theorem ONote.sub_nfBelow {o₁ : ONote} {o₂ : ONote} {b : Ordinal.{0}} :
ONote.NF o₂ONote.NFBelow (o₁ - o₂) b
instance ONote.sub_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.NF (o₁ - o₂)
@[simp]
theorem ONote.repr_sub (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.repr (o₁ - o₂) = -
def ONote.mul :

Multiplication of ordinal notations (correct only for normal input)

Equations
Instances For
theorem ONote.oadd_mul (e₁ : ONote) (n₁ : ℕ+) (a₁ : ONote) (e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote) :
ONote.oadd e₁ n₁ a₁ * ONote.oadd e₂ n₂ a₂ = if e₂ = 0 then ONote.oadd e₁ (n₁ * n₂) a₁ else ONote.oadd (e₁ + e₂) n₂ (ONote.oadd e₁ n₁ a₁ * a₂)
theorem ONote.oadd_mul_nfBelow {e₁ : ONote} {n₁ : ℕ+} {a₁ : ONote} {b₁ : Ordinal.{0}} (h₁ : ONote.NFBelow (ONote.oadd e₁ n₁ a₁) b₁) {o₂ : ONote} {b₂ : Ordinal.{0}} :
ONote.NFBelow o₂ b₂ONote.NFBelow (ONote.oadd e₁ n₁ a₁ * o₂) ( + b₂)
instance ONote.mul_nf (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.NF (o₁ * o₂)
@[simp]
theorem ONote.repr_mul (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.repr (o₁ * o₂) = *

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

Equations
Instances For
def ONote.split :
ONote

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

Equations
Instances For
def ONote.scale (x : ONote) :

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

Equations
Instances For

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

Instances For
def ONote.opowAux (e : ONote) (a0 : ONote) (a : ONote) :
ONote

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

Equations
Instances For
def ONote.opowAux2 (o₂ : ONote) (o₁ : ) :

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

Instances For
def ONote.opow (o₁ : ONote) (o₂ : ONote) :

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

Instances For
theorem ONote.opow_def (o₁ : ONote) (o₂ : ONote) :
o₁ ^ o₂ = ONote.opowAux2 o₂ ()
theorem ONote.split_eq_scale_split' {o : ONote} {o' : ONote} {m : } [] :
= (o', m) = (ONote.scale 1 o', m)
theorem ONote.nf_repr_split' {o : ONote} {o' : ONote} {m : } [] :
= (o', m)ONote.NF o' = + m
theorem ONote.scale_eq_mul (x : ONote) [] (o : ONote) [] :
= ONote.oadd x 1 0 * o
instance ONote.nf_scale (x : ONote) [] (o : ONote) [] :
@[simp]
theorem ONote.repr_scale (x : ONote) [] (o : ONote) [] :
theorem ONote.nf_repr_split {o : ONote} {o' : ONote} {m : } [] (h : = (o', m)) :
ONote.NF o' = + m
theorem ONote.split_dvd {o : ONote} {o' : ONote} {m : } [] (h : = (o', m)) :
theorem ONote.split_add_lt {o : ONote} {e : ONote} {n : ℕ+} {a : ONote} {m : } [] (h : = (ONote.oadd e n a, m)) :
+ m <
@[simp]
theorem ONote.mulNat_eq_mul (n : ) (o : ONote) :
= o * n
instance ONote.nf_mulNat (o : ONote) [] (n : ) :
instance ONote.nf_opowAux (e : ONote) (a0 : ONote) (a : ONote) [] [ONote.NF a0] [] (k : ) (m : ) :
ONote.NF (ONote.opowAux e a0 a k m)
instance ONote.nf_opow (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.NF (o₁ ^ o₂)
theorem ONote.scale_opowAux (e : ONote) (a0 : ONote) (a : ONote) [] [ONote.NF a0] [] (k : ) (m : ) :
theorem ONote.repr_opow_aux₁ {e : ONote} {a : ONote} [Ne : ] [Na : ] {a' : Ordinal.{0}} (e0 : 0) (h : ) (aa : = a') (n : ℕ+) :
( * n + a') ^ Ordinal.omega =
theorem ONote.repr_opow_aux₂ {a0 : ONote} {a' : ONote} [N0 : ONote.NF a0] [Na' : ONote.NF a'] (m : ) (d : ) (e0 : 0) (h : + m < ) (n : ℕ+) (k : ) :
let R := ONote.repr (ONote.opowAux 0 a0 (ONote.oadd a0 n a' * m) k m); (k 0R < () ^ ) () ^ k * ( * n + ) + R = ( * n + + m) ^
theorem ONote.repr_opow (o₁ : ONote) (o₂ : ONote) [ONote.NF o₁] [ONote.NF o₂] :
ONote.repr (o₁ ^ o₂) = ^

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
• One or more equations did not get rendered due to their size.
Instances For

The property satisfied by fundamentalSequence 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
Instances For
theorem ONote.fundamentalSequenceProp_inr (o : ONote) (f : ) :
(∀ (i : ), f i < f (i + 1) f i < o (ONote.NF (f i))) ∀ (a : Ordinal.{0}), a < i, a < ONote.repr (f i)

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
• One or more equations did not get rendered due to their size.
Instances For
theorem ONote.fastGrowing_def {o : ONote} {x : ()} (e : ) :
= match (motive := (x : ()) → ) x, (_ : ) with | Sum.inl none, x => Nat.succ | Sum.inl (some a), x => fun i => )^[i] i | , x => fun i => ONote.fastGrowing (f i) i
theorem ONote.fastGrowing_zero' (o : ONote) (h : ) :
theorem ONote.fastGrowing_succ (o : ONote) {a : ONote} (h : ) :
= fun i => )^[i] i
theorem ONote.fastGrowing_limit (o : ONote) {f : } (h : ) :
= fun i => ONote.fastGrowing (f i) i
@[simp]
theorem ONote.fastGrowing_one :
= fun n => 2 * n
@[simp]
theorem ONote.fastGrowing_two :
= fun 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.

Instances For

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

Instances For
instance NONote.NF (o : NONote) :
def NONote.mk (o : ONote) [h : ] :

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

Instances For
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.)

Instances For
theorem NONote.lt_wf :
WellFounded fun x x_1 => x < x_1

Convert a natural number to an ordinal notation

Instances For
def NONote.cmp (a : NONote) (b : NONote) :

Compare ordinal notations

Instances For
def NONote.below (a : NONote) (b : NONote) :

Asserts that repr a < ω ^ repr b. Used in NONote.recOn

Instances For
def NONote.oadd (e : NONote) (n : ℕ+) (a : NONote) (h : ) :

The oadd pseudo-constructor for NONote

Instances For
def NONote.recOn {C : NONoteSort u_1} (o : NONote) (H0 : C 0) (H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : ) → C eC aC (NONote.oadd e 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.

Instances For

theorem NONote.repr_add (a : NONote) (b : NONote) :
NONote.repr (a + b) =

Subtraction of ordinal notations

theorem NONote.repr_sub (a : NONote) (b : NONote) :
NONote.repr (a - b) =

Multiplication of ordinal notations

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

Exponentiation of ordinal notations

Instances For