Deleting the least Cantor term

The least additive-principal term of a natural ordinal, its deletion, and the properties of that deletion: it splits a nonzero grade as removeLeastTerm a + leastTerm a = a, it drops cantorTermCount by exactly one, and it agrees with NatOrdinal.removeNat _ 1 exactly on the grades carrying a finite part.

noncomputable def NatOrdinal.leastTerm (a : NatOrdinal) : NatOrdinal

The final additive-principal term of the ordinal, or zero when the ordinal is zero.

Equations

• a.leastTerm = NatOrdinal.of ((NatOrdinal.val a).additivePrincipalTerms.getLastD 0)

noncomputable def NatOrdinal.removeLeastTerm (a : NatOrdinal) : NatOrdinal

The ordinal obtained by removing the final additive-principal term from its Cantor decomposition.

Equations

• a.removeLeastTerm = NatOrdinal.of (NatOrdinal.val a).additivePrincipalTerms.dropLast.sum

@[simp]

theorem NatOrdinal.val_removeLeastTerm (a : NatOrdinal) : val a.removeLeastTerm = (val a).additivePrincipalTerms.dropLast.sum

@[simp]

theorem NatOrdinal.leastTerm_zero : leastTerm 0 = 0

@[simp]

theorem NatOrdinal.removeLeastTerm_zero : removeLeastTerm 0 = 0

theorem NatOrdinal.additivePrincipalTerms_ne_nil {a : NatOrdinal} (ha : a ≠ 0) : (val a).additivePrincipalTerms ≠ []

theorem NatOrdinal.val_leastTerm {a : NatOrdinal} (hne : (val a).additivePrincipalTerms ≠ []) : val a.leastTerm = (val a).additivePrincipalTerms.getLast hne

theorem NatOrdinal.isAdditivelyPrincipal_leastTerm {a : NatOrdinal} (ha : a ≠ 0) : (val a.leastTerm).IsAdditivelyPrincipal

theorem NatOrdinal.removeLeastTerm_add_leastTerm (a : NatOrdinal) : a.removeLeastTerm + a.leastTerm = a

theorem NatOrdinal.cantorTermCount_leastTerm {a : NatOrdinal} (ha : a ≠ 0) : a.leastTerm.cantorTermCount = 1

theorem NatOrdinal.cantorTermCount_removeLeastTerm {a : NatOrdinal} (ha : a ≠ 0) : a.removeLeastTerm.cantorTermCount + 1 = a.cantorTermCount

theorem NatOrdinal.cantorTermCount_removeLeastTerm_lt {a : NatOrdinal} (ha : a ≠ 0) : a.removeLeastTerm.cantorTermCount < a.cantorTermCount

theorem NatOrdinal.removeLeastTerm_eq_zero_iff {a : NatOrdinal} (ha : a ≠ 0) : a.removeLeastTerm = 0 ↔ a.cantorTermCount = 1

theorem NatOrdinal.cantorTermCount_eq_one_iff {a : NatOrdinal} (ha : a ≠ 0) : a.cantorTermCount = 1 ↔ (val a).IsAdditivelyPrincipal

The least term of a sum

theorem NatOrdinal.val_leastTerm_mem {a : NatOrdinal} (ha : a ≠ 0) : val a.leastTerm ∈ (val a).additivePrincipalTerms

theorem NatOrdinal.val_leastTerm_le_of_mem {a : NatOrdinal} (ha : a ≠ 0) {y : Ordinal.{u}} (hy : y ∈ (val a).additivePrincipalTerms) : val a.leastTerm ≤ y

theorem NatOrdinal.leastTerm_add {a b : NatOrdinal} (ha : a ≠ 0) (hb : b ≠ 0) : (a + b).leastTerm = min a.leastTerm b.leastTerm

theorem NatOrdinal.removeLeastTerm_add_of_leastTerm_le {a b : NatOrdinal} (ha : a ≠ 0) (hb : b ≠ 0) (hle : a.leastTerm ≤ b.leastTerm) : (a + b).removeLeastTerm = a.removeLeastTerm + b

theorem NatOrdinal.nsmul_ne_zero_of_ne_zero {a : NatOrdinal} (ha : a ≠ 0) {r : ℕ} (hr : 1 ≤ r) : r • a ≠ 0

theorem NatOrdinal.leastTerm_nsmul {a : NatOrdinal} (ha : a ≠ 0) {r : ℕ} (hr : 1 ≤ r) : (r • a).leastTerm = a.leastTerm

theorem NatOrdinal.removeLeastTerm_nsmul {a : NatOrdinal} (ha : a ≠ 0) {r : ℕ} (hr : 1 ≤ r) : a.removeLeastTerm + (r - 1) • a = (r • a).removeLeastTerm

theorem NatOrdinal.removeLeastTerm_add_of_leastTerm_ge {a b : NatOrdinal} (ha : a ≠ 0) (hb : b ≠ 0) (hle : b.leastTerm ≤ a.leastTerm) : (a + b).removeLeastTerm = a + b.removeLeastTerm

theorem NatOrdinal.leastTerm_eq_self_of_isAdditivelyPrincipal {a : NatOrdinal} (ha : a ≠ 0) (hprin : (val a).IsAdditivelyPrincipal) : a.leastTerm = a

Deletion on a sum with a repeated summand

The grade k • alpha + beta has least Cantor term min (leastTerm alpha) (leastTerm beta), by leastTerm_add and leastTerm_nsmul, so deletion falls on whichever side attains the minimum. The two lemmas below name the two outcomes, and the third says the second outcome can repeat only finitely often.

theorem NatOrdinal.removeLeastTerm_nsmul_add_of_le {alpha beta : NatOrdinal} (ha : alpha ≠ 0) (hb : beta ≠ 0) {k : ℕ} (hk : 1 ≤ k) (hle : alpha.leastTerm ≤ beta.leastTerm) : (k • alpha + beta).removeLeastTerm = alpha.removeLeastTerm + (k - 1) • alpha + beta

theorem NatOrdinal.removeLeastTerm_nsmul_add_of_ge {alpha beta : NatOrdinal} (ha : alpha ≠ 0) (hb : beta ≠ 0) {k : ℕ} (hk : 1 ≤ k) (hle : beta.leastTerm ≤ alpha.leastTerm) : (k • alpha + beta).removeLeastTerm = k • alpha + beta.removeLeastTerm

theorem NatOrdinal.exists_iterate_removeLeastTerm (alpha beta : NatOrdinal) : ∃ (j : ℕ), removeLeastTerm^[j] beta = 0 ∨ alpha.leastTerm ≤ (removeLeastTerm^[j] beta).leastTerm

theorem NatOrdinal.removeLeastTerm_add_one_eq_self_iff {a : NatOrdinal} : a.removeLeastTerm + 1 = a ↔ a.leastTerm = 1

theorem NatOrdinal.add_ne_of_isAdditivelyPrincipal {a i j : NatOrdinal} (ha : (val a).IsAdditivelyPrincipal) (hi : i ≠ 0) (hj : j ≠ 0) : i + j ≠ a

theorem NatOrdinal.leastTerm_ne_zero {a : NatOrdinal} (ha : a ≠ 0) : a.leastTerm ≠ 0

theorem NatOrdinal.one_le_leastTerm {a : NatOrdinal} (ha : a ≠ 0) : 1 ≤ a.leastTerm

@[simp]

theorem NatOrdinal.leastTerm_one : leastTerm 1 = 1

@[simp]

theorem NatOrdinal.removeLeastTerm_one : removeLeastTerm 1 = 0

theorem NatOrdinal.removeLeastTerm_add_one {a : NatOrdinal} : (a + 1).removeLeastTerm = a

theorem NatOrdinal.exists_lt_removeLeastTerm_not_lt {a : NatOrdinal} (ha : 1 < a.leastTerm) : ∃ (b : NatOrdinal), b ≠ 0 ∧ b < a ∧ a.removeLeastTerm ≤ b.removeLeastTerm

Deletion is not strictly monotone below a grade whose least Cantor term exceeds 1: the grade removeLeastTerm a + 1 is strictly below a, yet deletion sends it to removeLeastTerm a rather than below it.

Agreement with the finite-part operation

theorem NatOrdinal.additivePrincipalTerms_eq_append_one {a : NatOrdinal} (ha : 0 < a.constantCoeff) : (val (a.removeNat 1)).additivePrincipalTerms ++ [1] = (val a).additivePrincipalTerms

theorem NatOrdinal.leastTerm_eq_one_of_constantCoeff_pos {a : NatOrdinal} (ha : 0 < a.constantCoeff) : a.leastTerm = 1

theorem NatOrdinal.removeLeastTerm_eq_removeNat_one {a : NatOrdinal} (ha : 0 < a.constantCoeff) : a.removeLeastTerm = a.removeNat 1