Fixed points of normal functions

We prove various statements about the fixed points of normal ordinal functions. We state them in three forms: as statements about type-indexed families of normal functions, as statements about ordinal-indexed families of normal functions, and as statements about a single normal function. For the most part, the first case encompasses the others.

Moreover, we prove some lemmas about the fixed points of specific normal functions.

Main definitions and results

• nfpFamily, nfpBFamily, nfp: the next fixed point of a (family of) normal function(s).
• fp_family_unbounded, fp_bfamily_unbounded, fp_unbounded: the (common) fixed points of a (family of) normal function(s) are unbounded in the ordinals.
• deriv_add_eq_mul_omega_add: a characterization of the derivative of addition.
• deriv_mul_eq_opow_omega_mul: a characterization of the derivative of multiplication.

Fixed points of type-indexed families of ordinals

def Ordinal.nfpFamily {ι : Type u} (f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1} ) (a : Ordinal.{max u u_1} ) : Ordinal.{max u_1 u}

The next common fixed point, at least a, for a family of normal functions.

This is defined for any family of functions, as the supremum of all values reachable by applying finitely many functions in the family to a.

Ordinal.nfpFamily_fp shows this is a fixed point, Ordinal.le_nfpFamily shows it's at least a, and Ordinal.nfpFamily_le_fp shows this is the least ordinal with these properties.

Equations

• Ordinal.nfpFamily f a = Ordinal.sup (List.foldr f a)

theorem Ordinal.nfpFamily_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) (a : Ordinal.{max u v} ) : Ordinal.nfpFamily f a = Ordinal.sup (List.foldr f a)

theorem Ordinal.foldr_le_nfpFamily {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) (a : Ordinal.{max u v} ) (l : List ι) : List.foldr f a l ≤ Ordinal.nfpFamily f a

theorem Ordinal.le_nfpFamily {ι : Type u} (f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1} ) (a : Ordinal.{max u u_1} ) : a ≤ Ordinal.nfpFamily f a

theorem Ordinal.lt_nfpFamily {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } : a < Ordinal.nfpFamily f b ↔ ∃ (l : List ι), a < List.foldr f b l

theorem Ordinal.nfpFamily_le_iff {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max u v} } {b : Ordinal.{max v u} } : Ordinal.nfpFamily f a ≤ b ↔ ∀ (l : List ι), List.foldr f a l ≤ b

theorem Ordinal.nfpFamily_le {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } : (∀ (l : List ι), List.foldr f a l ≤ b) → Ordinal.nfpFamily f a ≤ b

theorem Ordinal.nfpFamily_monotone {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (hf : ∀ (i : ι), Monotone (f i)) : Monotone (Ordinal.nfpFamily f)

theorem Ordinal.apply_lt_nfpFamily {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max v u} } (hb : b < Ordinal.nfpFamily f a) (i : ι) : f i b < Ordinal.nfpFamily f a

theorem Ordinal.apply_lt_nfpFamily_iff {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } [Nonempty ι] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } : (∀ (i : ι), f i b < Ordinal.nfpFamily f a) ↔ b < Ordinal.nfpFamily f a

theorem Ordinal.nfpFamily_le_apply {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } [Nonempty ι] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } : (∃ (i : ι), Ordinal.nfpFamily f a ≤ f i b) ↔ Ordinal.nfpFamily f a ≤ b

theorem Ordinal.nfpFamily_le_fp {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Monotone (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (ab : a ≤ b) (h : ∀ (i : ι), f i b ≤ b) : Ordinal.nfpFamily f a ≤ b

theorem Ordinal.nfpFamily_fp {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {i : ι} (H : Ordinal.IsNormal (f i)) (a : Ordinal.{max u v} ) : f i (Ordinal.nfpFamily f a) = Ordinal.nfpFamily f a

theorem Ordinal.apply_le_nfpFamily {ι : Type u} [hι : Nonempty ι] {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } : (∀ (i : ι), f i b ≤ Ordinal.nfpFamily f a) ↔ b ≤ Ordinal.nfpFamily f a

theorem Ordinal.nfpFamily_eq_self {ι : Type u} {f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1} } {a : Ordinal.{max u u_1} } (h : ∀ (i : ι), f i a = a) : Ordinal.nfpFamily f a = a

theorem Ordinal.fp_family_unbounded {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) : Set.Unbounded (fun (x x_1 : Ordinal.{max u v} ) => x < x_1) (⋂ (i : ι), Function.fixedPoints (f i))

A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points.

def Ordinal.derivFamily {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) (o : Ordinal.{max u v} ) : Ordinal.{max u v}

The derivative of a family of normal functions is the sequence of their common fixed points.

This is defined for all functions such that Ordinal.derivFamily_zero, Ordinal.derivFamily_succ, and Ordinal.derivFamily_limit are satisfied.

Equations

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

@[simp]

theorem Ordinal.derivFamily_zero {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) : Ordinal.derivFamily f 0 = Ordinal.nfpFamily f 0

@[simp]

theorem Ordinal.derivFamily_succ {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) (o : Ordinal.{max u v} ) : Ordinal.derivFamily f (Order.succ o) = Ordinal.nfpFamily f (Order.succ (Ordinal.derivFamily f o))

theorem Ordinal.derivFamily_limit {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v} ) {o : Ordinal.{max u v} } : Ordinal.IsLimit o → Ordinal.derivFamily f o = Ordinal.bsup o fun (a : Ordinal.{max u v} ) (x : a < o) => Ordinal.derivFamily f a

theorem Ordinal.derivFamily_isNormal {ι : Type u} (f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1} ) : Ordinal.IsNormal (Ordinal.derivFamily f)

theorem Ordinal.derivFamily_fp {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } {i : ι} (H : Ordinal.IsNormal (f i)) (o : Ordinal.{max u v} ) : f i (Ordinal.derivFamily f o) = Ordinal.derivFamily f o

theorem Ordinal.le_iff_derivFamily {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } : (∀ (i : ι), f i a ≤ a) ↔ ∃ (o : Ordinal.{max u v} ), Ordinal.derivFamily f o = a

theorem Ordinal.fp_iff_derivFamily {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } : (∀ (i : ι), f i a = a) ↔ ∃ (o : Ordinal.{max u v} ), Ordinal.derivFamily f o = a

theorem Ordinal.derivFamily_eq_enumOrd {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : ι), Ordinal.IsNormal (f i)) : Ordinal.derivFamily f = Ordinal.enumOrd (⋂ (i : ι), Function.fixedPoints (f i))

For a family of normal functions, Ordinal.derivFamily enumerates the common fixed points.

Fixed points of ordinal-indexed families of ordinals

def Ordinal.nfpBFamily (o : Ordinal.{u_1}) (f : (b : Ordinal.{u_1}) → b < o → Ordinal.{max u_1 u_2} → Ordinal.{max u_1 u_2} ) : Ordinal.{max u_2 u_1} → Ordinal.{max u_2 u_1}

The next common fixed point, at least a, for a family of normal functions indexed by ordinals.

This is defined as Ordinal.nfpFamily of the type-indexed family associated to f.

Equations

• Ordinal.nfpBFamily o f = Ordinal.nfpFamily (Ordinal.familyOfBFamily o f)

theorem Ordinal.nfpBFamily_eq_nfpFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} ) : Ordinal.nfpBFamily o f = Ordinal.nfpFamily (Ordinal.familyOfBFamily o f)

theorem Ordinal.foldr_le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} ) (a : Ordinal.{max u v} ) (l : List (Quotient.out o).α) : List.foldr (Ordinal.familyOfBFamily o f) a l ≤ Ordinal.nfpBFamily o f a

theorem Ordinal.le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} ) (a : Ordinal.{max v u} ) : a ≤ Ordinal.nfpBFamily o f a

theorem Ordinal.lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } : a < Ordinal.nfpBFamily o f b ↔ ∃ (l : List (Quotient.out o).α), a < List.foldr (Ordinal.familyOfBFamily o f) b l

theorem Ordinal.nfpBFamily_le_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } : Ordinal.nfpBFamily o f a ≤ b ↔ ∀ (l : List (Quotient.out o).α), List.foldr (Ordinal.familyOfBFamily o f) a l ≤ b

theorem Ordinal.nfpBFamily_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } : (∀ (l : List (Quotient.out o).α), List.foldr (Ordinal.familyOfBFamily o f) a l ≤ b) → Ordinal.nfpBFamily o f a ≤ b

theorem Ordinal.nfpBFamily_monotone {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (hf : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)) : Monotone (Ordinal.nfpBFamily o f)

theorem Ordinal.apply_lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } (hb : b < Ordinal.nfpBFamily o f a) (i : Ordinal.{u}) (hi : i < o) : f i hi b < Ordinal.nfpBFamily o f a

theorem Ordinal.apply_lt_nfpBFamily_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (ho : o ≠ 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < Ordinal.nfpBFamily o f a) ↔ b < Ordinal.nfpBFamily o f a

theorem Ordinal.nfpBFamily_le_apply {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (ho : o ≠ 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } : (∃ (i : Ordinal.{u}) (hi : i < o), Ordinal.nfpBFamily o f a ≤ f i hi b) ↔ Ordinal.nfpBFamily o f a ≤ b

theorem Ordinal.nfpBFamily_le_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (ab : a ≤ b) (h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ b) : Ordinal.nfpBFamily o f a ≤ b

theorem Ordinal.nfpBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max v u} ) : f i hi (Ordinal.nfpBFamily o f a) = Ordinal.nfpBFamily o f a

theorem Ordinal.apply_le_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (ho : o ≠ 0) (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi b ≤ Ordinal.nfpBFamily o f a) ↔ b ≤ Ordinal.nfpBFamily o f a

theorem Ordinal.nfpBFamily_eq_self {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {a : Ordinal.{max u v} } (h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) : Ordinal.nfpBFamily o f a = a

theorem Ordinal.fp_bfamily_unbounded {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) : Set.Unbounded (fun (x x_1 : Ordinal.{max u v} ) => x < x_1) (⋂ (i : Ordinal.{u}), ⋂ (hi : i < o), Function.fixedPoints (f i hi))

A generalization of the fixed point lemma for normal functions: any family of normal functions has an unbounded set of common fixed points.

def Ordinal.derivBFamily (o : Ordinal.{u_1}) (f : (b : Ordinal.{u_1}) → b < o → Ordinal.{max u_1 u_2} → Ordinal.{max u_1 u_2} ) : Ordinal.{max u_2 u_1} → Ordinal.{max u_2 u_1}

The derivative of a family of normal functions is the sequence of their common fixed points.

This is defined as Ordinal.derivFamily of the type-indexed family associated to f.

Equations

• Ordinal.derivBFamily o f = Ordinal.derivFamily (Ordinal.familyOfBFamily o f)

theorem Ordinal.derivBFamily_eq_derivFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} ) : Ordinal.derivBFamily o f = Ordinal.derivFamily (Ordinal.familyOfBFamily o f)

theorem Ordinal.derivBFamily_isNormal {o : Ordinal.{u_1}} (f : (b : Ordinal.{u_1}) → b < o → Ordinal.{max u_1 u_2} → Ordinal.{max u_1 u_2} ) : Ordinal.IsNormal (Ordinal.derivBFamily o f)

theorem Ordinal.derivBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max u v} ) : f i hi (Ordinal.derivBFamily o f a) = Ordinal.derivBFamily o f a

theorem Ordinal.le_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ (b : Ordinal.{max v u} ), Ordinal.derivBFamily o f b = a

theorem Ordinal.fp_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max u v} } : (∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) ↔ ∃ (b : Ordinal.{max v u} ), Ordinal.derivBFamily o f b = a

theorem Ordinal.derivBFamily_eq_enumOrd {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v} } (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) : Ordinal.derivBFamily o f = Ordinal.enumOrd (⋂ (i : Ordinal.{u}), ⋂ (hi : i < o), Function.fixedPoints (f i hi))

For a family of normal functions, Ordinal.derivBFamily enumerates the common fixed points.

Fixed points of a single function

def Ordinal.nfp (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.{u_1} → Ordinal.{u_1}

The next fixed point function, the least fixed point of the normal function f, at least a.

This is defined as ordinal.nfpFamily applied to a family consisting only of f.

Equations

• Ordinal.nfp f = Ordinal.nfpFamily fun (x : Unit) => f

theorem Ordinal.nfp_eq_nfpFamily (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.nfp f = Ordinal.nfpFamily fun (x : Unit) => f

@[simp]

theorem Ordinal.sup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) : (fun (a : Ordinal.{u}) => Ordinal.sup fun (n : ℕ) => f^[n] a) = Ordinal.nfp f

theorem Ordinal.iterate_le_nfp (f : Ordinal.{u_1} → Ordinal.{u_1}) (a : Ordinal.{u_1}) (n : ℕ) : f^[n] a ≤ Ordinal.nfp f a

theorem Ordinal.le_nfp (f : Ordinal.{u_1} → Ordinal.{u_1}) (a : Ordinal.{u_1}) : a ≤ Ordinal.nfp f a

theorem Ordinal.lt_nfp {f : Ordinal.{u} → Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} : a < Ordinal.nfp f b ↔ ∃ (n : ℕ), a < f^[n] b

theorem Ordinal.nfp_le_iff {f : Ordinal.{u} → Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} : Ordinal.nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

theorem Ordinal.nfp_le {f : Ordinal.{u} → Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} : (∀ (n : ℕ), f^[n] a ≤ b) → Ordinal.nfp f a ≤ b

@[simp]

theorem Ordinal.nfp_id : Ordinal.nfp id = id

theorem Ordinal.nfp_monotone {f : Ordinal.{u} → Ordinal.{u}} (hf : Monotone f) : Monotone (Ordinal.nfp f)

theorem Ordinal.IsNormal.apply_lt_nfp {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : f b < Ordinal.nfp f a ↔ b < Ordinal.nfp f a

theorem Ordinal.IsNormal.nfp_le_apply {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : Ordinal.nfp f a ≤ f b ↔ Ordinal.nfp f a ≤ b

theorem Ordinal.nfp_le_fp {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Monotone f) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (ab : a ≤ b) (h : f b ≤ b) : Ordinal.nfp f a ≤ b

theorem Ordinal.IsNormal.nfp_fp {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) (a : Ordinal.{u_1}) : f (Ordinal.nfp f a) = Ordinal.nfp f a

theorem Ordinal.IsNormal.apply_le_nfp {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : f b ≤ Ordinal.nfp f a ↔ b ≤ Ordinal.nfp f a

theorem Ordinal.nfp_eq_self {f : Ordinal.{u_1} → Ordinal.{u_1}} {a : Ordinal.{u_1}} (h : f a = a) : Ordinal.nfp f a = a

theorem Ordinal.fp_unbounded {f : Ordinal.{u} → Ordinal.{u}} (H : Ordinal.IsNormal f) : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) (Function.fixedPoints f)

The fixed point lemma for normal functions: any normal function has an unbounded set of fixed points.

def Ordinal.deriv (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.{u_1} → Ordinal.{u_1}

The derivative of a normal function f is the sequence of fixed points of f.

This is defined as Ordinal.derivFamily applied to a trivial family consisting only of f.

Equations

• Ordinal.deriv f = Ordinal.derivFamily fun (x : Unit) => f

theorem Ordinal.deriv_eq_derivFamily (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.deriv f = Ordinal.derivFamily fun (x : Unit) => f

@[simp]

theorem Ordinal.deriv_zero (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.deriv f 0 = Ordinal.nfp f 0

@[simp]

theorem Ordinal.deriv_succ (f : Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}) : Ordinal.deriv f (Order.succ o) = Ordinal.nfp f (Order.succ (Ordinal.deriv f o))

theorem Ordinal.deriv_limit (f : Ordinal.{u} → Ordinal.{u}) {o : Ordinal.{u}} : Ordinal.IsLimit o → Ordinal.deriv f o = Ordinal.bsup o fun (a : Ordinal.{u}) (x : a < o) => Ordinal.deriv f a

theorem Ordinal.deriv_isNormal (f : Ordinal.{u_1} → Ordinal.{u_1}) : Ordinal.IsNormal (Ordinal.deriv f)

theorem Ordinal.deriv_id_of_nfp_id {f : Ordinal.{u_1} → Ordinal.{u_1}} (h : Ordinal.nfp f = id) : Ordinal.deriv f = id

theorem Ordinal.IsNormal.deriv_fp {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) (o : Ordinal.{u_1}) : f (Ordinal.deriv f o) = Ordinal.deriv f o

theorem Ordinal.IsNormal.le_iff_deriv {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_1}} : f a ≤ a ↔ ∃ (o : Ordinal.{u_1}), Ordinal.deriv f o = a

theorem Ordinal.IsNormal.fp_iff_deriv {f : Ordinal.{u_1} → Ordinal.{u_1}} (H : Ordinal.IsNormal f) {a : Ordinal.{u_1}} : f a = a ↔ ∃ (o : Ordinal.{u_1}), Ordinal.deriv f o = a

theorem Ordinal.deriv_eq_enumOrd {f : Ordinal.{u} → Ordinal.{u}} (H : Ordinal.IsNormal f) : Ordinal.deriv f = Ordinal.enumOrd (Function.fixedPoints f)

Ordinal.deriv enumerates the fixed points of a normal function.

theorem Ordinal.deriv_eq_id_of_nfp_eq_id {f : Ordinal.{u_1} → Ordinal.{u_1}} (h : Ordinal.nfp f = id) : Ordinal.deriv f = id

Fixed points of addition

@[simp]

theorem Ordinal.nfp_add_zero (a : Ordinal.{u_1}) : Ordinal.nfp (fun (x : Ordinal.{u_1}) => a + x) 0 = a * Ordinal.omega

theorem Ordinal.nfp_add_eq_mul_omega {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (hba : b ≤ a * Ordinal.omega) : Ordinal.nfp (fun (x : Ordinal.{u_1}) => a + x) b = a * Ordinal.omega

theorem Ordinal.add_eq_right_iff_mul_omega_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a + b = b ↔ a * Ordinal.omega ≤ b

theorem Ordinal.add_le_right_iff_mul_omega_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a + b ≤ b ↔ a * Ordinal.omega ≤ b

theorem Ordinal.deriv_add_eq_mul_omega_add (a : Ordinal.{u}) (b : Ordinal.{u}) : Ordinal.deriv (fun (x : Ordinal.{u}) => a + x) b = a * Ordinal.omega + b

Fixed points of multiplication

@[simp]

theorem Ordinal.nfp_mul_one {a : Ordinal.{u_1}} (ha : 0 < a) : Ordinal.nfp (fun (x : Ordinal.{u_1}) => a * x) 1 = a ^ Ordinal.omega

@[simp]

theorem Ordinal.nfp_mul_zero (a : Ordinal.{u_1}) : Ordinal.nfp (fun (x : Ordinal.{u_1}) => a * x) 0 = 0

@[simp]

theorem Ordinal.nfp_zero_mul : Ordinal.nfp (HMul.hMul 0) = id

@[simp]

theorem Ordinal.deriv_mul_zero : Ordinal.deriv (HMul.hMul 0) = id

theorem Ordinal.nfp_mul_eq_opow_omega {a : Ordinal.{u}} {b : Ordinal.{u}} (hb : 0 < b) (hba : b ≤ a ^ Ordinal.omega) : Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) b = a ^ Ordinal.omega

theorem Ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right {a : Ordinal.{u}} {b : Ordinal.{u}} (hab : a * b = b) : b = 0 ∨ a ^ Ordinal.omega ≤ b

theorem Ordinal.mul_eq_right_iff_opow_omega_dvd {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : a * b = b ↔ a ^ Ordinal.omega ∣ b

theorem Ordinal.mul_le_right_iff_opow_omega_dvd {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (ha : 0 < a) : a * b ≤ b ↔ a ^ Ordinal.omega ∣ b

theorem Ordinal.nfp_mul_opow_omega_add {a : Ordinal.{u}} {c : Ordinal.{u}} (b : Ordinal.{u}) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ Ordinal.omega) : Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) (a ^ Ordinal.omega * b + c) = a ^ Ordinal.omega * Order.succ b

theorem Ordinal.deriv_mul_eq_opow_omega_mul {a : Ordinal.{u}} (ha : 0 < a) (b : Ordinal.{u}) : Ordinal.deriv (fun (x : Ordinal.{u}) => a * x) b = a ^ Ordinal.omega * b