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, exponentiation) 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 a 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 we make it a separate definition NF.

Notation for 0

Equations
@[simp]
theorem ONote.zero_def :

Notation for 1

Equations

Notation for ω

Equations
noncomputable def ONote.repr :

The ordinal denoted by a notation

Equations
@[simp]
theorem ONote.repr_zero :
repr 0 = 0

Print an ordinal notation

Equations
def ONote.repr' (prec : ) :

Print an ordinal notation

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

Convert a Nat into an ordinal

Equations
@[simp]
theorem ONote.ofNat_zero :
0 = 0
@[simp]
theorem ONote.ofNat_succ (n : ) :
n.succ = oadd 0 n.succPNat 0
@[instance 100]
instance ONote.nat (n : ) :
Equations
@[simp]
theorem ONote.ofNat_one :
1 = 1
@[simp]
theorem ONote.repr_ofNat (n : ) :
(↑n).repr = n
@[simp]
theorem ONote.repr_one :
repr 1 = 1
theorem ONote.oadd_pos (e : ONote) (n : ℕ+) (a : ONote) :
0 < e.oadd n a

Comparison of ordinal notations:

ω ^ e₁ * n₁ + a₁ is less than ω ^ e₂ * n₂ + a₂ when either e₁ < e₂, or e₁ = e₂ and n₁ < n₂, or e₁ = e₂, n₁ = n₂, and a₁ < a₂.

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

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

class ONote.NF (o : ONote) :

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}} :
    e.NFa.NFBelow e.repre.repr < b(e.oadd n a).NFBelow b
    theorem ONote.NFBelow.fst {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
    e.NF
    theorem ONote.NF.fst {e : ONote} {n : ℕ+} {a : ONote} :
    (e.oadd n a).NFe.NF
    theorem ONote.NFBelow.snd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
    theorem ONote.NF.snd' {e : ONote} {n : ℕ+} {a : ONote} :
    (e.oadd n a).NFa.NFBelow e.repr
    theorem ONote.NF.snd {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :
    a.NF
    theorem ONote.NF.oadd {e a : ONote} (h₁ : e.NF) (n : ℕ+) (h₂ : a.NFBelow e.repr) :
    (e.oadd n a).NF
    instance ONote.NF.oadd_zero (e : ONote) (n : ℕ+) [h : e.NF] :
    (e.oadd n 0).NF
    theorem ONote.NFBelow.lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
    e.repr < b
    theorem ONote.NFBelow_zero {o : ONote} :
    o.NFBelow 0 o = 0
    theorem ONote.NF.zero_of_zero {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) (e0 : e = 0) :
    a = 0
    theorem ONote.NFBelow.mono {o : ONote} {b₁ b₂ : Ordinal.{0}} (bb : b₁ b₂) (h : o.NFBelow b₁) :
    o.NFBelow b₂
    theorem ONote.NF.below_of_lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (H : e.repr < b) :
    (e.oadd n a).NF(e.oadd n a).NFBelow b
    theorem ONote.nfBelow_ofNat (n : ) :
    (↑n).NFBelow 1
    instance ONote.nf_ofNat (n : ) :
    (↑n).NF
    theorem ONote.oadd_lt_oadd_1 {e₁ : ONote} {n₁ : ℕ+} {o₁ e₂ : ONote} {n₂ : ℕ+} {o₂ : ONote} (h₁ : (e₁.oadd n₁ o₁).NF) (h : e₁ < e₂) :
    e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂
    theorem ONote.oadd_lt_oadd_2 {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+} (h₁ : (e.oadd n₁ o₁).NF) (h : n₁ < n₂) :
    e.oadd n₁ o₁ < e.oadd n₂ o₂
    theorem ONote.oadd_lt_oadd_3 {e : ONote} {n : ℕ+} {a₁ a₂ : ONote} (h : a₁ < a₂) :
    e.oadd n a₁ < e.oadd n a₂
    theorem ONote.cmp_compares (a b : ONote) [a.NF] [b.NF] :
    (a.cmp b).Compares a b
    theorem ONote.repr_inj {a b : ONote} [a.NF] [b.NF] :
    a.repr = b.repr a = b
    theorem ONote.NF.of_dvd_omega0_opow {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) (d : Ordinal.omega0 ^ b (e.oadd n a).repr) :
    theorem ONote.NF.of_dvd_omega0 {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :

    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.

    Equations
    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

    Equations
    def ONote.add :
    ONoteONoteONote

    Addition of ordinal notations (correct only for normal input)

    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 = e.addAux n (a + o)
    def ONote.sub :
    ONoteONoteONote

    Subtraction of ordinal notations (correct only for normal input)

    Equations
    theorem ONote.add_nfBelow {b : Ordinal.{0}} {o₁ o₂ : ONote} :
    o₁.NFBelow bo₂.NFBelow b(o₁ + o₂).NFBelow b
    instance ONote.add_nf (o₁ o₂ : ONote) [o₁.NF] [o₂.NF] :
    (o₁ + o₂).NF
    @[simp]
    theorem ONote.repr_add (o₁ o₂ : ONote) [o₁.NF] [o₂.NF] :
    (o₁ + o₂).repr = o₁.repr + o₂.repr
    theorem ONote.sub_nfBelow {o₁ o₂ : ONote} {b : Ordinal.{0}} :
    o₁.NFBelow bo₂.NF(o₁ - o₂).NFBelow b
    instance ONote.sub_nf (o₁ o₂ : ONote) [o₁.NF] [o₂.NF] :
    (o₁ - o₂).NF
    @[simp]
    theorem ONote.repr_sub (o₁ o₂ : ONote) [o₁.NF] [o₂.NF] :
    (o₁ - o₂).repr = o₁.repr - o₂.repr
    def ONote.mul :
    ONoteONoteONote

    Multiplication of ordinal notations (correct only for normal input)

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

    Calculate division and remainder of o mod ω:

    split' o = (a, n) means o = ω * a + n.

    Equations

    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

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

    Equations
    def ONote.opowAux (e a0 a : ONote) :
    ONote

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

    Equations
    def ONote.opowAux2 (o₂ : ONote) (o₁ : ONote × ) :

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

    Equations
    def ONote.opow (o₁ o₂ : ONote) :

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

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

    Given an ordinal, returns:

    • inl none for 0
    • inl (some a) for a + 1
    • inr f for a limit ordinal a, where f i is a sequence converging to a
    Equations

    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
    Equations
    theorem ONote.fundamentalSequenceProp_inr (o : ONote) (f : ONote) :
    o.FundamentalSequenceProp (Sum.inr f) o.repr.IsLimit (∀ (i : ), f i < f (i + 1) f i < o (o.NF(f i).NF)) a < o.repr, ∃ (i : ), a < (f i).repr
    @[irreducible]

    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.
    theorem ONote.fastGrowing_def {o : ONote} {x : Option ONote (ONote)} (e : o.fundamentalSequence = x) :
    o.fastGrowing = match (motive := (x : Option ONote (ONote)) → o.FundamentalSequenceProp x) x, with | Sum.inl none, x => Nat.succ | Sum.inl (some a), x => fun (i : ) => a.fastGrowing^[i] i | Sum.inr f, x => fun (i : ) => (f i).fastGrowing i
    theorem ONote.fastGrowing_limit (o : ONote) {f : ONote} (h : o.fundamentalSequence = Sum.inr f) :
    o.fastGrowing = fun (i : ) => (f i).fastGrowing i
    @[simp]
    theorem ONote.fastGrowing_one :
    fastGrowing 1 = fun (n : ) => 2 * n
    @[simp]
    theorem ONote.fastGrowing_two :
    fastGrowing 2 = fun (n : ) => 2 ^ n * n

    We can extend the fast growing hierarchy one more step to ε₀ itself, using ω ^ (ω ^ (⋯ ^ ω)) 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

    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
    instance NONote.NF (o : NONote) :
    (↑o).NF
    def NONote.mk (o : ONote) [h : o.NF] :

    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
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    theorem NONote.lt_wf :
    WellFounded fun (x1 x2 : NONote) => x1 < x2

    Convert a natural number to an ordinal notation

    Equations

    Compare ordinal notations

    Equations
    theorem NONote.cmp_compares (a b : NONote) :
    (a.cmp b).Compares a b
    def NONote.below (a b : NONote) :

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

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

    The oadd pseudo-constructor for NONote

    Equations
    def NONote.recOn {C : NONoteSort u_1} (o : NONote) (H0 : C 0) (H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C eC aC (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
    • One or more equations did not get rendered due to their size.

    Addition of ordinal notations

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

    Subtraction of ordinal notations

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

    Multiplication of ordinal notations

    Equations
    theorem NONote.repr_mul (a b : NONote) :
    (a * b).repr = a.repr * b.repr

    Exponentiation of ordinal notations

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