Jakobs' order through the Hessenberg sum

Jakobs' order on finite multisets of ordinals, read as the order of ordinals through the Hessenberg (natural) sum h s = ♯_{x ∈ s} ω ^ x. The natural sum is defined through Cantor normal form coefficients: a ♯ b = CNF.eval ω (CNF.coeff ω a + CNF.coeff ω b).

Main results

• hval_add: h (s + t) = h s ♯ h t.
• jakobsLT_iff_hval_lt: jakobsLT s t ↔ h s < h t; hence hval_injective.
• image_hval: {h s | ∀ x ∈ s, x ≤ Λ} = Set.Iio (ω ^ (Λ + 1)).
• omega0_opow_add_one_lt_epsilon_zero: Λ < ε₀ → ω ^ (Λ + 1) < ε₀.

Related

Mathlib no longer contains the natural sum of ordinals: it was moved out of Mathlib.SetTheory.Ordinal.NaturalOps to the combinatorial games library (https://github.com/vihdzp/combinatorial-games, CombinatorialGames.NatOrdinal), where it is defined by recursion on NatOrdinal. The nadd here is defined independently, inside Mathlib, through Cantor normal form coefficients; no equivalence between the two definitions is proved here.

References

• F. Jakobs, PhD thesis, 2019, Thm. 1.1.3; Dubrovin–Gräter–Hanke, Prop. 2.1.

Natural (Hessenberg) sum via CNF coefficients

theorem DGH.coeff_omega0_lt (o e : Ordinal.{u}) : (Ordinal.CNF.coeff Ordinal.omega0 o) e < Ordinal.omega0

noncomputable def DGH.nadd (a b : Ordinal.{u}) : Ordinal.{u}

Natural (Hessenberg) sum: add Cantor-normal-form coefficients base ω.

Equations

• DGH.nadd a b = Ordinal.CNF.eval Ordinal.omega0 (Ordinal.CNF.coeff Ordinal.omega0 a + Ordinal.CNF.coeff Ordinal.omega0 b)

def DGH.«term_♯_» : Lean.TrailingParserDescr

Natural (Hessenberg) sum: add Cantor-normal-form coefficients base ω.

Equations

• DGH.«term_♯_» = Lean.ParserDescr.trailingNode `DGH.«term_♯_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♯ ") (Lean.ParserDescr.cat `term 66))

theorem DGH.coeff_nadd (a b : Ordinal.{u}) : Ordinal.CNF.coeff Ordinal.omega0 (nadd a b) = Ordinal.CNF.coeff Ordinal.omega0 a + Ordinal.CNF.coeff Ordinal.omega0 b

theorem DGH.add_comm_of_lt_omega0 {x y : Ordinal.{u}} (hx : x < Ordinal.omega0) (hy : y < Ordinal.omega0) : x + y = y + x

Ordinal + is commutative below ω (natural numbers).

theorem DGH.nadd_comm (a b : Ordinal.{u}) : nadd a b = nadd b a

theorem DGH.nadd_assoc (a b c : Ordinal.{u}) : nadd (nadd a b) c = nadd a (nadd b c)

@[simp]

theorem DGH.nadd_zero (a : Ordinal.{u}) : nadd a 0 = a

Multisets of ordinals as CNF coefficient functions

noncomputable def DGH.cf (s : Multiset Ordinal.{u}) : Ordinal.{u} →₀ Ordinal.{u}

cf s x = count x s, as a finitely supported Ordinal-valued function.

Equations

• DGH.cf s = Finsupp.mapRange (fun (n : ℕ) => ↑n) ⋯ (Multiset.toFinsupp s)

@[simp]

theorem DGH.cf_apply (s : Multiset Ordinal.{u}) (x : Ordinal.{u}) : (cf s) x = ↑(Multiset.count x s)

theorem DGH.mem_support_cf {s : Multiset Ordinal.{u}} {x : Ordinal.{u}} : x ∈ (cf s).support ↔ x ∈ s

theorem DGH.cf_add (s t : Multiset Ordinal.{u}) : cf (s + t) = cf s + cf t

@[simp]

theorem DGH.cf_zero : cf 0 = 0

theorem DGH.cf_replicate (n : ℕ) (x : Ordinal.{u}) : cf (Multiset.replicate n x) = Finsupp.single x ↑n

theorem DGH.cf_lt (s : Multiset Ordinal.{u}) (x : Ordinal.{u}) : (cf s) x < Ordinal.omega0

noncomputable def DGH.hval (s : Multiset Ordinal.{u}) : Ordinal.{u}

h s = ♯_{x ∈ s} ω ^ x (the Hessenberg sum of the ω ^ x).

Equations

• DGH.hval s = Ordinal.CNF.eval Ordinal.omega0 (DGH.cf s)

theorem DGH.hval_add (s t : Multiset Ordinal.{u}) : hval (s + t) = nadd (hval s) (hval t)

(1) h is a monoid homomorphism (Multiset Ordinal, +) → (Ordinal, ♯).

@[simp]

theorem DGH.hval_zero : hval 0 = 0

theorem DGH.hval_replicate (n : ℕ) (x : Ordinal.{u}) : hval (Multiset.replicate n x) = Ordinal.omega0 ^ x * ↑n

theorem DGH.hval_singleton (x : Ordinal.{u}) : hval {x} = Ordinal.omega0 ^ x

theorem DGH.hval_add_of_le {s t : Multiset Ordinal.{u}} (hst : ∀ a ∈ s, ∀ b ∈ t, b ≤ a) : hval (s + t) = hval s + hval t

When every element of t is ≤ every element of s, ♯ is ordinary +.

theorem DGH.hval_lt {s : Multiset Ordinal.{u}} {x : Ordinal.{u}} (hs : ∀ a ∈ s, a < x) : hval s < Ordinal.omega0 ^ x

theorem DGH.decomp (s : Multiset Ordinal.{u}) (x : Ordinal.{u}) : s = Multiset.filter (fun (x_1 : Ordinal.{u}) => x < x_1) s + (Multiset.filter (fun (x_1 : Ordinal.{u}) => x_1 = x) s + Multiset.filter (fun (x_1 : Ordinal.{u}) => x_1 < x) s)

theorem DGH.hval_split (s : Multiset Ordinal.{u}) (x : Ordinal.{u}) : hval s = hval (Multiset.filter (fun (x_1 : Ordinal.{u}) => x < x_1) s) + (Ordinal.omega0 ^ x * ↑(Multiset.count x s) + hval (Multiset.filter (fun (x_1 : Ordinal.{u}) => x_1 < x) s))

(2) Jakobs' order is the ordinal order through h

theorem DGH.hval_lt_of_jakobsLT {s t : Multiset Ordinal.{u}} (h : jakobsLT s t) : hval s < hval t

theorem DGH.jakobsLT_iff_hval_lt {s t : Multiset Ordinal.{u}} : jakobsLT s t ↔ hval s < hval t

(2) s <_J t ↔ h s < h t.

theorem DGH.hval_injective : Function.Injective hval

(3) Image of N(Λ)

theorem DGH.exists_cf (f : Ordinal.{u} →₀ Ordinal.{u}) (hf : ∀ (e : Ordinal.{u}), f e < Ordinal.omega0) : ∃ (s : Multiset Ordinal.{u}), cf s = f

theorem DGH.image_hval (Λ : Ordinal.{u}) : {β : Ordinal.{u} | ∃ (s : Multiset Ordinal.{u}), (∀ x ∈ s, x ≤ Λ) ∧ hval s = β} = Set.Iio (Ordinal.omega0 ^ (Λ + 1))

(3) {h s | all x ∈ s are ≤ Λ} = [0, ω ^ (Λ + 1)).

theorem DGH.exists_equiv_jakobs (Λ : Ordinal.{u}) : ∃ (e : { s : Multiset Ordinal.{u} // ∀ x ∈ s, x ≤ Λ } ≃ ↑(Set.Iio (Ordinal.omega0 ^ (Λ + 1)))), ∀ (s t : { s : Multiset Ordinal.{u} // ∀ x ∈ s, x ≤ Λ }), jakobsLT ↑s ↑t ↔ ↑(e s) < ↑(e t)

(2)+(3) packaged: N(Λ) with Jakobs' order is order-isomorphic to ω ^ (Λ + 1).

theorem DGH.omega0_opow_add_one_lt_epsilon_zero {Λ : Ordinal.{u}} (h : Λ < Ordinal.epsilon 0) : Ordinal.omega0 ^ (Λ + 1) < Ordinal.epsilon 0

Corollary: for Λ < ε₀, the order type ω ^ (Λ + 1) of N(Λ) stays below ε₀.