Documentation

Mathlib.SetTheory.Ordinal.CantorNormalForm

Cantor Normal Form #

The Cantor normal form of an ordinal is generally defined as its base ω expansion, with its non-zero exponents in decreasing order. Here, we more generally define a base b expansion Ordinal.CNF in this manner, which is well-behaved for any b ≥ 2.

Implementation notes #

We implement Ordinal.CNF as an association list, where keys are exponents and values are coefficients. This is because this structure intrinsically reflects two key properties of the Cantor normal form:

Todo #

noncomputable def Ordinal.CNFRec (b : Ordinal.{u_2}) {C : Ordinal.{u_2}Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o 0C (o % b ^ Ordinal.log b o)C o) (o : Ordinal.{u_2}) :
C o

Inducts on the base b expansion of an ordinal.

Equations
Instances For
    @[simp]
    theorem Ordinal.CNFRec_zero {C : Ordinal.{u_2}Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o 0C (o % b ^ Ordinal.log b o)C o) :
    Ordinal.CNFRec b H0 H 0 = H0
    theorem Ordinal.CNFRec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2}Sort u_1} (ho : o 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o 0C (o % b ^ Ordinal.log b o)C o) :
    Ordinal.CNFRec b H0 H o = H o ho (Ordinal.CNFRec b H0 H (o % b ^ Ordinal.log b o))

    The Cantor normal form of an ordinal o is the list of coefficients and exponents in the base-b expansion of o.

    We special-case CNF 0 o = CNF 1 o = [(0, o)] for o ≠ 0.

    CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

    Instances For
      @[simp]
      theorem Ordinal.CNF_ne_zero {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (ho : o 0) :

      Recursive definition for the Cantor normal form.

      theorem Ordinal.zero_CNF {o : Ordinal.{u_1}} (ho : o 0) :
      Ordinal.CNF 0 o = [(0, o)]
      theorem Ordinal.one_CNF {o : Ordinal.{u_1}} (ho : o 0) :
      Ordinal.CNF 1 o = [(0, o)]
      theorem Ordinal.CNF_of_le_one {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hb : b 1) (ho : o 0) :
      Ordinal.CNF b o = [(0, o)]
      theorem Ordinal.CNF_of_lt {b : Ordinal.{u_1}} {o : Ordinal.{u_1}} (ho : o 0) (hb : o < b) :
      Ordinal.CNF b o = [(0, o)]
      theorem Ordinal.CNF_foldr (b : Ordinal.{u_1}) (o : Ordinal.{u_1}) :
      List.foldr (fun p r => b ^ p.fst * p.snd + r) 0 (Ordinal.CNF b o) = o

      Evaluating the Cantor normal form of an ordinal returns the ordinal.

      Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

      theorem Ordinal.CNF_fst_le {b : Ordinal.{u}} {o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} (h : x Ordinal.CNF b o) :
      x.fst o

      Every exponent in the Cantor normal form CNF b o is less or equal to o.

      theorem Ordinal.CNF_lt_snd {b : Ordinal.{u}} {o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} :
      x Ordinal.CNF b o0 < x.snd

      Every coefficient in a Cantor normal form is positive.

      theorem Ordinal.CNF_snd_lt {b : Ordinal.{u}} {o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} :
      x Ordinal.CNF b ox.snd < b

      Every coefficient in the Cantor normal form CNF b o is less than b.

      theorem Ordinal.CNF_sorted (b : Ordinal.{u_1}) (o : Ordinal.{u_1}) :
      List.Sorted (fun x x_1 => x > x_1) (List.map Prod.fst (Ordinal.CNF b o))

      The exponents of the Cantor normal form are decreasing.