# 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 : ι) (a : Ordinal.{max u u_1} ) :

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
Instances For
theorem Ordinal.nfpFamily_eq_sup {ι : Type u} (f : ι) (a : Ordinal.{max u v} ) :
theorem Ordinal.foldr_le_nfpFamily {ι : Type u} (f : ι) (a : Ordinal.{max u v} ) (l : List ι) :
theorem Ordinal.le_nfpFamily {ι : Type u} (f : ι) (a : Ordinal.{max u u_1} ) :
a
theorem Ordinal.lt_nfpFamily {ι : Type u} {f : ι} {a : Ordinal.{max v u} } {b : Ordinal.{max u v} } :
a < ∃ (l : List ι), a < List.foldr f b l
theorem Ordinal.nfpFamily_le_iff {ι : Type u} {f : ι} {a : Ordinal.{max u v} } {b : Ordinal.{max v u} } :
b ∀ (l : List ι), List.foldr f a l b
theorem Ordinal.nfpFamily_le {ι : Type u} {f : ι} {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
(∀ (l : List ι), List.foldr f a l b) b
theorem Ordinal.nfpFamily_monotone {ι : Type u} {f : ι} (hf : ∀ (i : ι), Monotone (f i)) :
theorem Ordinal.apply_lt_nfpFamily {ι : Type u} {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max v u} } (hb : b < ) (i : ι) :
f i b <
theorem Ordinal.apply_lt_nfpFamily_iff {ι : Type u} {f : ι} [] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
(∀ (i : ι), f i b < ) b <
theorem Ordinal.nfpFamily_le_apply {ι : Type u} {f : ι} [] (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
(∃ (i : ι), f i b) b
theorem Ordinal.nfpFamily_le_fp {ι : Type u} {f : ι} (H : ∀ (i : ι), Monotone (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } (ab : a b) (h : ∀ (i : ι), f i b b) :
b
theorem Ordinal.nfpFamily_fp {ι : Type u} {f : ι} {i : ι} (H : Ordinal.IsNormal (f i)) (a : Ordinal.{max u v} ) :
f i =
theorem Ordinal.apply_le_nfpFamily {ι : Type u} [hι : ] {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
(∀ (i : ι), f i b ) b
theorem Ordinal.nfpFamily_eq_self {ι : Type u} {f : ι} {a : Ordinal.{max u u_1} } (h : ∀ (i : ι), f i a = a) :
= a
theorem Ordinal.fp_family_unbounded {ι : Type u} {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) :
Set.Unbounded (fun (x1 x2 : Ordinal.{max u v} ) => x1 < x2) (⋂ (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 : ι) (o : 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.
Instances For
@[simp]
theorem Ordinal.derivFamily_zero {ι : Type u} (f : ι) :
@[simp]
theorem Ordinal.derivFamily_succ {ι : Type u} (f : ι) (o : Ordinal.{max u v} ) :
=
theorem Ordinal.derivFamily_limit {ι : Type u} (f : ι) {o : Ordinal.{max u v} } :
o.IsLimit = o.bsup fun (a : Ordinal.{max u v} ) (x : a < o) =>
theorem Ordinal.derivFamily_isNormal {ι : Type u} (f : ι) :
theorem Ordinal.derivFamily_fp {ι : Type u} {f : ι} {i : ι} (H : Ordinal.IsNormal (f i)) (o : Ordinal.{max u v} ) :
f i =
theorem Ordinal.le_iff_derivFamily {ι : Type u} {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } :
(∀ (i : ι), f i a a) ∃ (o : Ordinal.{max u v} ), = a
theorem Ordinal.fp_iff_derivFamily {ι : Type u} {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) {a : Ordinal.{max u v} } :
(∀ (i : ι), f i a = a) ∃ (o : Ordinal.{max u v} ), = a
theorem Ordinal.derivFamily_eq_enumOrd {ι : Type u} {f : ι} (H : ∀ (i : ι), Ordinal.IsNormal (f i)) :
= 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) :

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
Instances For
theorem Ordinal.nfpBFamily_eq_nfpFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o) :
o.nfpBFamily f = Ordinal.nfpFamily (o.familyOfBFamily f)
theorem Ordinal.foldr_le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o) (a : Ordinal.{max u v} ) (l : List o.toType) :
List.foldr (o.familyOfBFamily f) a l o.nfpBFamily f a
theorem Ordinal.le_nfpBFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o) (a : Ordinal.{max v u} ) :
a o.nfpBFamily f a
theorem Ordinal.lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } :
a < o.nfpBFamily f b ∃ (l : List o.toType), a < List.foldr (o.familyOfBFamily f) b l
theorem Ordinal.nfpBFamily_le_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } :
o.nfpBFamily f a b ∀ (l : List o.toType), List.foldr (o.familyOfBFamily f) a l b
theorem Ordinal.nfpBFamily_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {a : Ordinal.{max u v} } {b : Ordinal.{max u v} } :
(∀ (l : List o.toType), List.foldr (o.familyOfBFamily f) a l b)o.nfpBFamily f a b
theorem Ordinal.nfpBFamily_monotone {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (hf : ∀ (i : Ordinal.{u}) (hi : i < o), Monotone (f i hi)) :
Monotone (o.nfpBFamily f)
theorem Ordinal.apply_lt_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) {a : Ordinal.{max v u} } {b : Ordinal.{max v u} } (hb : b < o.nfpBFamily f a) (i : Ordinal.{u}) (hi : i < o) :
f i hi b < o.nfpBFamily f a
theorem Ordinal.apply_lt_nfpBFamily_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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 < o.nfpBFamily f a) b < o.nfpBFamily f a
theorem Ordinal.nfpBFamily_le_apply {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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), o.nfpBFamily f a f i hi b) o.nfpBFamily f a b
theorem Ordinal.nfpBFamily_le_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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) :
o.nfpBFamily f a b
theorem Ordinal.nfpBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max v u} ) :
f i hi (o.nfpBFamily f a) = o.nfpBFamily f a
theorem Ordinal.apply_le_nfpBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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 o.nfpBFamily f a) b o.nfpBFamily f a
theorem Ordinal.nfpBFamily_eq_self {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {a : Ordinal.{max u v} } (h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi a = a) :
o.nfpBFamily f a = a
theorem Ordinal.fp_bfamily_unbounded {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) :
Set.Unbounded (fun (x1 x2 : Ordinal.{max u v} ) => x1 < x2) (⋂ (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) :

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
Instances For
theorem Ordinal.derivBFamily_eq_derivFamily {o : Ordinal.{u}} (f : (b : Ordinal.{u}) → b < o) :
o.derivBFamily f = Ordinal.derivFamily (o.familyOfBFamily f)
theorem Ordinal.derivBFamily_isNormal {o : Ordinal.{u_1}} (f : (b : Ordinal.{u_1}) → b < o) :
Ordinal.IsNormal (o.derivBFamily f)
theorem Ordinal.derivBFamily_fp {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} {i : Ordinal.{u}} {hi : i < o} (H : Ordinal.IsNormal (f i hi)) (a : Ordinal.{max u v} ) :
f i hi (o.derivBFamily f a) = o.derivBFamily f a
theorem Ordinal.le_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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} ), o.derivBFamily f b = a
theorem Ordinal.fp_iff_derivBFamily {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (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} ), o.derivBFamily f b = a
theorem Ordinal.derivBFamily_eq_enumOrd {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o} (H : ∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) :
o.derivBFamily 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 : ) :

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
Instances For
theorem Ordinal.nfp_eq_nfpFamily (f : ) :
= Ordinal.nfpFamily fun (x : Unit) => f
theorem Ordinal.sup_iterate_eq_nfp (f : ) (a : Ordinal.{u}) :
(Ordinal.sup fun (n : ) => f^[n] a) =
theorem Ordinal.iterate_le_nfp (f : ) (a : Ordinal.{u_1}) (n : ) :
f^[n] a
theorem Ordinal.le_nfp (f : ) (a : Ordinal.{u_1}) :
a
theorem Ordinal.lt_nfp {f : } {a : Ordinal.{u}} {b : Ordinal.{u}} :
a < ∃ (n : ), a < f^[n] b
theorem Ordinal.nfp_le_iff {f : } {a : Ordinal.{u}} {b : Ordinal.{u}} :
b ∀ (n : ), f^[n] a b
theorem Ordinal.nfp_le {f : } {a : Ordinal.{u}} {b : Ordinal.{u}} :
(∀ (n : ), f^[n] a b) b
@[simp]
theorem Ordinal.nfp_id :
= id
theorem Ordinal.nfp_monotone {f : } (hf : ) :
theorem Ordinal.IsNormal.apply_lt_nfp {f : } (H : ) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
f b < b <
theorem Ordinal.IsNormal.nfp_le_apply {f : } (H : ) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
f b b
theorem Ordinal.nfp_le_fp {f : } (H : ) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (ab : a b) (h : f b b) :
b
theorem Ordinal.IsNormal.nfp_fp {f : } (H : ) (a : Ordinal.{u_1}) :
f (Ordinal.nfp f a) =
theorem Ordinal.IsNormal.apply_le_nfp {f : } (H : ) {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} :
f b b
theorem Ordinal.nfp_eq_self {f : } {a : Ordinal.{u_1}} (h : f a = a) :
= a
theorem Ordinal.fp_unbounded {f : } (H : ) :
Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2)

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

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
Instances For
@[simp]
theorem Ordinal.deriv_zero_right (f : ) :
=
theorem Ordinal.deriv_limit (f : ) {o : Ordinal.{u}} :
o.IsLimit = o.bsup fun (a : Ordinal.{u}) (x : a < o) =>
theorem Ordinal.deriv_id_of_nfp_id {f : } (h : = id) :
= id
theorem Ordinal.IsNormal.deriv_fp {f : } (H : ) (o : Ordinal.{u_1}) :
f (Ordinal.deriv f o) =
theorem Ordinal.IsNormal.le_iff_deriv {f : } (H : ) {a : Ordinal.{u_1}} :
f a a ∃ (o : Ordinal.{u_1}), = a
theorem Ordinal.IsNormal.fp_iff_deriv {f : } (H : ) {a : Ordinal.{u_1}} :
f a = a ∃ (o : Ordinal.{u_1}), = a
theorem Ordinal.deriv_eq_enumOrd {f : } (H : ) :

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

theorem Ordinal.deriv_eq_id_of_nfp_eq_id {f : } (h : = id) :
= id
@[simp]
theorem Ordinal.nfp_zero :
= id
@[simp]
theorem Ordinal.deriv_zero :
= 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 =
theorem Ordinal.nfp_add_eq_mul_omega {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (hba : b ) :
Ordinal.nfp (fun (x : Ordinal.{u_1}) => a + x) 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 =
@[simp]
theorem Ordinal.nfp_mul_zero (a : Ordinal.{u_1}) :
Ordinal.nfp (fun (x : Ordinal.{u_1}) => a * x) 0 = 0
theorem Ordinal.nfp_mul_eq_opow_omega {a : Ordinal.{u}} {b : Ordinal.{u}} (hb : 0 < b) (hba : b ) :
Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) 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 ) :
Ordinal.nfp (fun (x : Ordinal.{u}) => a * x) ( * b + c) =
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 = * b