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.

zero : ONote
oadd : ONote → ℕ+ → ONote → ONote

Instances For

instance instDecidableEqONote :

DecidableEq ONote

Equations

instDecidableEqONote = decEqONote✝

instance ONote.instZero :

Notation for 0

Equations

ONote.instZero = { zero := ONote.zero }

@[simp]

theorem ONote.zero_def :

instance ONote.instInhabited :

Inhabited ONote

Equations

ONote.instInhabited = { default := 0 }

instance ONote.instOne :

Notation for 1

Equations

ONote.instOne = { one := ONote.oadd 0 1 0 }

def ONote.omega :

Notation for ω

Equations

ONote.omega = ONote.oadd 1 1 0

Instances For

noncomputable def ONote.repr :

ONote → Ordinal.{0}

The ordinal denoted by a notation

Equations

ONote.zero.repr = 0
(e.oadd n a).repr = Ordinal.omega0 ^ e.repr * ↑↑n + a.repr

Instances For

def ONote.toString :

ONote → String

Print an ordinal notation

Equations

ONote.zero.toString = "0"
(e.oadd n ONote.zero).toString = ONote.toString_aux✝ e (↑n) e.toString
(e.oadd n a).toString = ONote.toString_aux✝ e (↑n) e.toString ++ " + " ++ a.toString

Instances For

def ONote.repr' (prec : ℕ) :

ONote → Lean.Format

Print an ordinal notation

Equations

One or more equations did not get rendered due to their size.
ONote.repr' prec ONote.zero = Std.Format.text "0"

Instances For

instance ONote.instToString :

Equations

ONote.instToString = { toString := ONote.toString }

instance ONote.instRepr :

Equations

ONote.instRepr = { reprPrec := fun (o : ONote) (prec : ℕ) => ONote.repr' prec o }

instance ONote.instPreorder :

Equations

ONote.instPreorder = Preorder.mk ONote.instPreorder.proof_1 ONote.instPreorder.proof_2 ONote.instPreorder.proof_3

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

instance ONote.instWellFoundedRelation :

WellFoundedRelation ONote

Equations

ONote.instWellFoundedRelation = { rel := fun (x1 x2 : ONote) => x1 < x2, wf := ONote.instWellFoundedRelation.proof_1 }

def ONote.ofNat :

Convert a Nat into an ordinal

Equations

↑0 = 0
↑n.succ = ONote.oadd 0 n.succPNat 0

Instances For

@[simp]

theorem ONote.ofNat_zero :

↑0 = 0

@[simp]

theorem ONote.ofNat_succ (n : ℕ) :

↑n.succ = ONote.oadd 0 n.succPNat 0

instance ONote.nat (n : ℕ) :

Equations

ONote.nat n = { ofNat := ↑n }

@[simp]

theorem ONote.ofNat_one :

↑1 = 1

@[simp]

theorem ONote.repr_ofNat (n : ℕ) :

(↑n).repr = ↑n

theorem ONote.repr_one :

(↑1).repr = ↑1

theorem ONote.omega0_le_oadd (e : ONote) (n : ℕ+) (a : ONote) :

Ordinal.omega0 ^ e.repr ≤ (e.oadd n a).repr

@[deprecated ONote.omega0_le_oadd]

theorem ONote.omega_le_oadd (e : ONote) (n : ℕ+) (a : ONote) :

Ordinal.omega0 ^ e.repr ≤ (e.oadd n a).repr

Alias of ONote.omega0_le_oadd.

theorem ONote.oadd_pos (e : ONote) (n : ℕ+) (a : ONote) :

0 < e.oadd n a

def ONote.cmp :

ONote → ONote → Ordering

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

ONote.zero.cmp ONote.zero = Ordering.eq
x✝.cmp ONote.zero = Ordering.gt
ONote.zero.cmp x = Ordering.lt
(e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = (e₁.cmp e₂).then ((cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))

Instances For

theorem ONote.eq_of_cmp_eq {o₁ o₂ : ONote} :

o₁.cmp o₂ = Ordering.eq → o₁ = o₂

theorem ONote.zero_lt_one :

0 < 1

inductive ONote.NFBelow :

ONote → Ordinal.{0} → Prop

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

zero {b : Ordinal.{0}} : ONote.NFBelow 0 b
oadd' {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}} : e.NFBelow eb → a.NFBelow e.repr → e.repr < b → (e.oadd n a).NFBelow b

Instances For

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.

out : Exists o.NFBelow

Instances

instance ONote.NF.zero :

theorem ONote.NFBelow.oadd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} :

e.NF → a.NFBelow e.repr → e.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).NF → e.NF

theorem ONote.NFBelow.snd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :

a.NFBelow e.repr

theorem ONote.NF.snd' {e : ONote} {n : ℕ+} {a : ONote} :

(e.oadd n a).NF → a.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.repr_lt {o : ONote} {b : Ordinal.{0}} (h : o.NFBelow b) :

o.repr < Ordinal.omega0 ^ b

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.NF.below_of_lt' {o : ONote} {b : Ordinal.{0}} :

o.repr < Ordinal.omega0 ^ b → o.NF → o.NFBelow b

theorem ONote.nfBelow_ofNat (n : ℕ) :

(↑n).NFBelow 1

instance ONote.nf_ofNat (n : ℕ) :

(↑n).NF

instance ONote.nf_one :

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

b ≤ e.repr ∧ Ordinal.omega0 ^ b ∣ a.repr

@[deprecated ONote.NF.of_dvd_omega0_opow]

theorem ONote.NF.of_dvd_omega_opow {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) (d : Ordinal.omega0 ^ b ∣ (e.oadd n a).repr) :

b ≤ e.repr ∧ Ordinal.omega0 ^ b ∣ a.repr

Alias of ONote.NF.of_dvd_omega0_opow.

theorem ONote.NF.of_dvd_omega0 {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :

Ordinal.omega0 ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ Ordinal.omega0 ∣ a.repr

@[deprecated ONote.NF.of_dvd_omega0]

theorem ONote.NF.of_dvd_omega {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :

Ordinal.omega0 ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ Ordinal.omega0 ∣ a.repr

Alias of ONote.NF.of_dvd_omega0.

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.

Equations

b.TopBelow ONote.zero = True
b.TopBelow (e.oadd n a) = (e.cmp b = Ordering.lt)

Instances For

instance ONote.decidableTopBelow :

DecidableRel ONote.TopBelow

Equations

One or more equations did not get rendered due to their size.

theorem ONote.nfBelow_iff_topBelow {b : ONote} [b.NF] {o : ONote} :

o.NFBelow b.repr ↔ o.NF ∧ b.TopBelow o

instance ONote.decidableNF :

DecidablePred ONote.NF

Equations

ONote.zero.decidableNF = isTrue ONote.NF.zero
(e.oadd n a).decidableNF = decidable_of_iff (e.NF ∧ a.NF ∧ e.TopBelow a) ⋯

def ONote.addAux (e : ONote) (n : ℕ+) (o : ONote) :

Auxiliary definition for add

Equations

e.addAux n ONote.zero = e.oadd n 0
e.addAux n (e'.oadd n' a') = match e.cmp e' with | Ordering.lt => e'.oadd n' a' | Ordering.eq => e.oadd (n + n') a' | Ordering.gt => e.oadd n (e'.oadd n' a')

Instances For

def ONote.add :

ONote → ONote → ONote

Addition of ordinal notations (correct only for normal input)

Equations

ONote.zero.add x✝ = x✝
(e.oadd n a).add x✝ = e.addAux n (a.add x✝)

Instances For

instance ONote.instAdd :

Equations

ONote.instAdd = { add := ONote.add }

@[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 :

ONote → ONote → ONote

Subtraction of ordinal notations (correct only for normal input)

Equations

One or more equations did not get rendered due to their size.
ONote.zero.sub x✝ = 0
x✝.sub ONote.zero = x✝

Instances For

instance ONote.instSub :

Equations

ONote.instSub = { sub := ONote.sub }

theorem ONote.add_nfBelow {b : Ordinal.{0}} {o₁ o₂ : ONote} :

o₁.NFBelow b → o₂.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 b → o₂.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 :

ONote → ONote → ONote

Multiplication of ordinal notations (correct only for normal input)

Equations

ONote.zero.mul x✝ = 0
x✝.mul ONote.zero = 0
(e₁.oadd n₁ a₁).mul (e₂.oadd n₂ a₂) = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ ((e₁.oadd n₁ a₁).mul a₂)

Instances For

instance ONote.instMul :

Equations

ONote.instMul = { mul := ONote.mul }

instance ONote.instMulZeroClass :

MulZeroClass ONote

Equations

ONote.instMulZeroClass = MulZeroClass.mk ONote.instMulZeroClass.proof_1 ONote.instMulZeroClass.proof_2

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

def ONote.split' :

ONote → ONote × ℕ

Calculate division and remainder of o mod ω:

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

Equations

ONote.zero.split' = (0, 0)
(e.oadd n a).split' = if e = 0 then (0, ↑n) else match a.split' with | (a', m) => ((e - 1).oadd n a', m)

Instances For

def ONote.split :

ONote → ONote × ℕ

Calculate division and remainder of o mod ω:

split o = (a, n) means o = a + n, where ω ∣ a.

Equations

ONote.zero.split = (0, 0)
(e.oadd n a).split = if e = 0 then (0, ↑n) else match a.split with | (a', m) => (e.oadd n a', m)

Instances For

def ONote.scale (x : ONote) :

ONote → ONote

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

Equations

x.scale ONote.zero = 0
x.scale (e.oadd n a) = (x + e).oadd n (x.scale a)

Instances For

def ONote.mulNat :

ONote → ℕ → ONote

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

Equations

ONote.zero.mulNat x✝ = 0
x✝.mulNat 0 = 0
(e.oadd n a).mulNat m.succ = e.oadd (n * m.succPNat) a

Instances For

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

ℕ → ℕ → ONote

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

Equations

e.opowAux a0 a x✝ 0 = 0
e.opowAux a0 a 0 m.succ = e.oadd m.succPNat 0
e.opowAux a0 a k.succ x✝ = (e + a0.mulNat k).scale a + e.opowAux a0 a k x✝

Instances For

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

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

Equations

One or more equations did not get rendered due to their size.
o₂.opowAux2 (ONote.zero, 0) = if o₂ = 0 then 1 else 0
o₂.opowAux2 (ONote.zero, 1) = 1
o₂.opowAux2 (ONote.zero, m.succ) = match o₂.split' with | (b', k) => b'.oadd (m.succPNat ^ k) 0

Instances For

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

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

Equations

o₁.opow o₂ = o₂.opowAux2 o₁.split

Instances For

instance ONote.instPow :

Pow ONote ONote

Equations

ONote.instPow = { pow := ONote.opow }

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 = (ONote.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] :

(x.scale o).repr = Ordinal.omega0 ^ x.repr * o.repr

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

Ordinal.omega0 ∣ o'.repr

theorem ONote.split_add_lt {o e : ONote} {n : ℕ+} {a : ONote} {m : ℕ} [o.NF] (h : o.split = (e.oadd n a, m)) :

a.repr + ↑m < Ordinal.omega0 ^ e.repr

@[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 * (ONote.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 : ℕ+) :

(Ordinal.omega0 ^ e.repr * ↑↑n + a') ^ Ordinal.omega0 = (Ordinal.omega0 ^ e.repr) ^ Ordinal.omega0

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 := (ONote.opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr; (k ≠ 0 → R < (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

def ONote.fundamentalSequence :

ONote → Option ONote ⊕ (ℕ → ONote)

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

One or more equations did not get rendered due to their size.
ONote.zero.fundamentalSequence = Sum.inl none

Instances For

def ONote.FundamentalSequenceProp (o : ONote) :

Option ONote ⊕ (ℕ → ONote) → Prop

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

o.FundamentalSequenceProp (Sum.inl none) = (o = 0)
o.FundamentalSequenceProp (Sum.inl (some a)) = (o.repr = Order.succ a.repr ∧ (o.NF → a.NF))
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)

Instances For

theorem ONote.fundamentalSequenceProp_inl_none (o : ONote) :

o.FundamentalSequenceProp (Sum.inl none) ↔ o = 0

theorem ONote.fundamentalSequenceProp_inl_some (o a : ONote) :

o.FundamentalSequenceProp (Sum.inl (some a)) ↔ o.repr = Order.succ a.repr ∧ (o.NF → a.NF)

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

theorem ONote.fundamentalSequence_has_prop (o : ONote) :

o.FundamentalSequenceProp o.fundamentalSequence

@[irreducible]

def ONote.fastGrowing :

ONote → ℕ → ℕ

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 : 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_zero' (o : ONote) (h : o.fundamentalSequence = Sum.inl none) :

o.fastGrowing = Nat.succ

theorem ONote.fastGrowing_succ (o : ONote) {a : ONote} (h : o.fundamentalSequence = Sum.inl (some a)) :

o.fastGrowing = fun (i : ℕ) => a.fastGrowing^[i] 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_zero :

ONote.fastGrowing 0 = Nat.succ

@[simp]

theorem ONote.fastGrowing_one :

ONote.fastGrowing 1 = fun (n : ℕ) => 2 * n

@[simp]

theorem ONote.fastGrowing_two :

ONote.fastGrowing 2 = fun (n : ℕ) => 2 ^ n * n

def ONote.fastGrowingε₀ (i : ℕ) :

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

ONote.fastGrowingε₀ i = ((fun (a : ONote) => a.oadd 1 0)^[i] 0).fastGrowing i

Instances For

theorem ONote.fastGrowingε₀_zero :

ONote.fastGrowingε₀ 0 = 1

theorem ONote.fastGrowingε₀_one :

ONote.fastGrowingε₀ 1 = 2

theorem ONote.fastGrowingε₀_two :

ONote.fastGrowingε₀ 2 = 2048

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

NONote = { o : ONote // o.NF }

Instances For

instance instDecidableEqNONote :

DecidableEq NONote

Equations

instDecidableEqNONote = id inferInstance

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

NONote.mk o = ⟨o, h⟩

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.

Equations

o.repr = (↑o).repr

Instances For

instance NONote.instToString :

ToString NONote

Equations

NONote.instToString = { toString := fun (x : NONote) => (↑x).toString }

instance NONote.instRepr :

Equations

NONote.instRepr = { reprPrec := fun (x : NONote) (prec : ℕ) => ONote.repr' prec ↑x }

instance NONote.instPreorder :

Preorder NONote

Equations

NONote.instPreorder = Preorder.mk NONote.instPreorder.proof_1 NONote.instPreorder.proof_2 NONote.instPreorder.proof_3

instance NONote.instZero :

Equations

NONote.instZero = { zero := ⟨0, ONote.NF.zero⟩ }

instance NONote.instInhabited :

Inhabited NONote

Equations

NONote.instInhabited = { default := 0 }

theorem NONote.lt_wf :

WellFounded fun (x1 x2 : NONote) => x1 < x2

instance NONote.instWellFoundedLT :

WellFoundedLT NONote

instance NONote.instWellFoundedRelation :

WellFoundedRelation NONote

Equations

NONote.instWellFoundedRelation = { rel := fun (x1 x2 : NONote) => x1 < x2, wf := NONote.lt_wf }

def NONote.ofNat (n : ℕ) :

Convert a natural number to an ordinal notation

Equations

NONote.ofNat n = ⟨↑n, ⋯⟩

Instances For

def NONote.cmp (a b : NONote) :

Compare ordinal notations

Equations

a.cmp b = (↑a).cmp ↑b

Instances For

theorem NONote.cmp_compares (a b : NONote) :

(a.cmp b).Compares a b

instance NONote.instLinearOrder :

LinearOrder NONote

Equations

NONote.instLinearOrder = linearOrderOfCompares NONote.cmp NONote.cmp_compares

def NONote.below (a b : NONote) :

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

Equations

a.below b = (↑a).NFBelow b.repr

Instances For

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

The oadd pseudo-constructor for NONote

Equations

e.oadd n a h = ⟨(↑e).oadd n ↑a, ⋯⟩

Instances For

def NONote.recOn {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

One or more equations did not get rendered due to their size.

Instances For

instance NONote.instAdd :

Addition of ordinal notations

Equations

NONote.instAdd = { add := fun (x y : NONote) => NONote.mk (↑x + ↑y) }

theorem NONote.repr_add (a b : NONote) :

(a + b).repr = a.repr + b.repr

instance NONote.instSub :

Subtraction of ordinal notations

Equations

NONote.instSub = { sub := fun (x y : NONote) => NONote.mk (↑x - ↑y) }

theorem NONote.repr_sub (a b : NONote) :

(a - b).repr = a.repr - b.repr

instance NONote.instMul :

Multiplication of ordinal notations

Equations

NONote.instMul = { mul := fun (x y : NONote) => NONote.mk (↑x * ↑y) }

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

x.opow y = NONote.mk (↑x ^ ↑y)

Instances For

theorem NONote.repr_opow (a b : NONote) :

(a.opow b).repr = a.repr ^ b.repr