# mathlib3documentation

set_theory.ordinal.fixed_point

# Fixed points of normal functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• nfp_family, nfp_bfamily, 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 #

noncomputable def ordinal.nfp_family {ι : Type u} (f : ι ) (a : ordinal) :

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.nfp_family_fp shows this is a fixed point, ordinal.le_nfp_family shows it's at least a, and ordinal.nfp_family_le_fp shows this is the least ordinal with these properties.

Equations
theorem ordinal.nfp_family_eq_sup {ι : Type u} (f : ι ) (a : ordinal) :
theorem ordinal.foldr_le_nfp_family {ι : Type u} (f : ι ) (a : ordinal) (l : list ι) :
a l
theorem ordinal.le_nfp_family {ι : Type u} (f : ι ) (a : ordinal) :
a
theorem ordinal.lt_nfp_family {ι : Type u} {f : ι } {a b : ordinal} :
a < (l : list ι), a < b l
theorem ordinal.nfp_family_le_iff {ι : Type u} {f : ι } {a b : ordinal} :
b (l : list ι), a l b
theorem ordinal.nfp_family_le {ι : Type u} {f : ι } {a b : ordinal} :
( (l : list ι), a l b) b
theorem ordinal.nfp_family_monotone {ι : Type u} {f : ι } (hf : (i : ι), monotone (f i)) :
theorem ordinal.apply_lt_nfp_family {ι : Type u} {f : ι } (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} (hb : b < ) (i : ι) :
f i b <
theorem ordinal.apply_lt_nfp_family_iff {ι : Type u} {f : ι } [nonempty ι] (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
( (i : ι), f i b < b <
theorem ordinal.nfp_family_le_apply {ι : Type u} {f : ι } [nonempty ι] (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
( (i : ι), f i b) b
theorem ordinal.nfp_family_le_fp {ι : Type u} {f : ι } (H : (i : ι), monotone (f i)) {a b : ordinal} (ab : a b) (h : (i : ι), f i b b) :
b
theorem ordinal.nfp_family_fp {ι : Type u} {f : ι } {i : ι} (H : ordinal.is_normal (f i)) (a : ordinal) :
f i a) =
theorem ordinal.apply_le_nfp_family {ι : Type u} [hι : nonempty ι] {f : ι } (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
( (i : ι), f i b b
theorem ordinal.nfp_family_eq_self {ι : Type u} {f : ι } {a : ordinal} (h : (i : ι), f i a = a) :
= a
theorem ordinal.fp_family_unbounded {ι : Type u} {f : ι } (H : (i : ι), ordinal.is_normal (f i)) :
( (i : ι), function.fixed_points (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.

noncomputable def ordinal.deriv_family {ι : Type u} (f : ι ) (o : ordinal) :

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.deriv_family_zero, ordinal.deriv_family_succ, and ordinal.deriv_family_limit are satisfied.

Equations
@[simp]
theorem ordinal.deriv_family_zero {ι : Type u} (f : ι ) :
@[simp]
theorem ordinal.deriv_family_succ {ι : Type u} (f : ι ) (o : ordinal) :
theorem ordinal.deriv_family_limit {ι : Type u} (f : ι ) {o : ordinal} :
o.is_limit = o.bsup (λ (a : ordinal) (_x : a < o),
theorem ordinal.deriv_family_is_normal {ι : Type u} (f : ι ) :
theorem ordinal.deriv_family_fp {ι : Type u} {f : ι } {i : ι} (H : ordinal.is_normal (f i)) (o : ordinal) :
f i o) =
theorem ordinal.le_iff_deriv_family {ι : Type u} {f : ι } (H : (i : ι), ordinal.is_normal (f i)) {a : ordinal} :
( (i : ι), f i a a) (o : ordinal),
theorem ordinal.fp_iff_deriv_family {ι : Type u} {f : ι } (H : (i : ι), ordinal.is_normal (f i)) {a : ordinal} :
( (i : ι), f i a = a) (o : ordinal),
theorem ordinal.deriv_family_eq_enum_ord {ι : Type u} {f : ι } (H : (i : ι), ordinal.is_normal (f i)) :

For a family of normal functions, ordinal.deriv_family enumerates the common fixed points.

### Fixed points of ordinal-indexed families of ordinals #

noncomputable def ordinal.nfp_bfamily (o : ordinal) (f : Π (b : ordinal), b < o ) :

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

This is defined as ordinal.nfp_family of the type-indexed family associated to f.

Equations
theorem ordinal.nfp_bfamily_eq_nfp_family {o : ordinal} (f : Π (b : ordinal), b < o ) :
theorem ordinal.foldr_le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < o ) (a : ordinal) (l : list (quotient.out o).α) :
a l o.nfp_bfamily f a
theorem ordinal.le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < o ) (a : ordinal) :
theorem ordinal.lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o } {a b : ordinal} :
a < o.nfp_bfamily f b (l : list (quotient.out o).α), a < b l
theorem ordinal.nfp_bfamily_le_iff {o : ordinal} {f : Π (b : ordinal), b < o } {a b : ordinal} :
o.nfp_bfamily f a b (l : list (quotient.out o).α), a l b
theorem ordinal.nfp_bfamily_le {o : ordinal} {f : Π (b : ordinal), b < o } {a b : ordinal} :
( (l : list (quotient.out o).α), a l b) o.nfp_bfamily f a b
theorem ordinal.nfp_bfamily_monotone {o : ordinal} {f : Π (b : ordinal), b < o } (hf : (i : ordinal) (hi : i < o), monotone (f i hi)) :
theorem ordinal.apply_lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a b : ordinal} (hb : b < o.nfp_bfamily f a) (i : ordinal) (hi : i < o) :
f i hi b < o.nfp_bfamily f a
theorem ordinal.apply_lt_nfp_bfamily_iff {o : ordinal} {f : Π (b : ordinal), b < o } (ho : o 0) (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a b : ordinal} :
( (i : ordinal) (hi : i < o), f i hi b < o.nfp_bfamily f a) b < o.nfp_bfamily f a
theorem ordinal.nfp_bfamily_le_apply {o : ordinal} {f : Π (b : ordinal), b < o } (ho : o 0) (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a b : ordinal} :
( (i : ordinal) (hi : i < o), o.nfp_bfamily f a f i hi b) o.nfp_bfamily f a b
theorem ordinal.nfp_bfamily_le_fp {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), monotone (f i hi)) {a b : ordinal} (ab : a b) (h : (i : ordinal) (hi : i < o), f i hi b b) :
theorem ordinal.nfp_bfamily_fp {o : ordinal} {f : Π (b : ordinal), b < o } {i : ordinal} {hi : i < o} (H : ordinal.is_normal (f i hi)) (a : ordinal) :
f i hi (o.nfp_bfamily f a) = o.nfp_bfamily f a
theorem ordinal.apply_le_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o } (ho : o 0) (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a b : ordinal} :
( (i : ordinal) (hi : i < o), f i hi b o.nfp_bfamily f a) b o.nfp_bfamily f a
theorem ordinal.nfp_bfamily_eq_self {o : ordinal} {f : Π (b : ordinal), b < o } {a : ordinal} (h : (i : ordinal) (hi : i < o), f i hi a = a) :
o.nfp_bfamily f a = a
theorem ordinal.fp_bfamily_unbounded {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) :
( (i : ordinal) (hi : i < o), function.fixed_points (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.

noncomputable def ordinal.deriv_bfamily (o : ordinal) (f : Π (b : ordinal), b < o ) :

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

This is defined as ordinal.deriv_family of the type-indexed family associated to f.

Equations
theorem ordinal.deriv_bfamily_eq_deriv_family {o : ordinal} (f : Π (b : ordinal), b < o ) :
theorem ordinal.deriv_bfamily_is_normal {o : ordinal} (f : Π (b : ordinal), b < o ) :
theorem ordinal.deriv_bfamily_fp {o : ordinal} {f : Π (b : ordinal), b < o } {i : ordinal} {hi : i < o} (H : ordinal.is_normal (f i hi)) (a : ordinal) :
f i hi (o.deriv_bfamily f a) = a
theorem ordinal.le_iff_deriv_bfamily {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a : ordinal} :
( (i : ordinal) (hi : i < o), f i hi a a) (b : ordinal), b = a
theorem ordinal.fp_iff_deriv_bfamily {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) {a : ordinal} :
( (i : ordinal) (hi : i < o), f i hi a = a) (b : ordinal), b = a
theorem ordinal.deriv_bfamily_eq_enum_ord {o : ordinal} {f : Π (b : ordinal), b < o } (H : (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) :
= ordinal.enum_ord ( (i : ordinal) (hi : i < o), function.fixed_points (f i hi))

For a family of normal functions, ordinal.deriv_bfamily enumerates the common fixed points.

### Fixed points of a single function #

noncomputable def ordinal.nfp (f : ordinal ordinal) :

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

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

Equations
@[simp]
theorem ordinal.sup_iterate_eq_nfp (f : ordinal ordinal) :
(λ (a : ordinal), ordinal.sup (λ (n : ), f^[n] a)) =
theorem ordinal.iterate_le_nfp (f : ordinal ordinal) (a : ordinal) (n : ) :
f^[n] a a
theorem ordinal.le_nfp (f : ordinal ordinal) (a : ordinal) :
a a
theorem ordinal.lt_nfp {f : ordinal ordinal} {a b : ordinal} :
a < b (n : ), a < f^[n] b
theorem ordinal.nfp_le_iff {f : ordinal ordinal} {a b : ordinal} :
a b (n : ), f^[n] a b
theorem ordinal.nfp_le {f : ordinal ordinal} {a b : ordinal} :
( (n : ), f^[n] a b) a b
@[simp]
theorem ordinal.nfp_id  :
theorem ordinal.nfp_le_fp {f : ordinal ordinal} (H : monotone f) {a b : ordinal} (ab : a b) (h : f b b) :
a b
theorem ordinal.nfp_eq_self {f : ordinal ordinal} {a : ordinal} (h : f a = a) :
a = a

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

noncomputable def ordinal.deriv (f : ordinal ordinal) :

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

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

Equations
@[simp]
theorem ordinal.deriv_zero (f : ordinal ordinal) :
= 0
@[simp]
theorem ordinal.deriv_limit (f : ordinal ordinal) {o : ordinal} :
o.is_limit = o.bsup (λ (a : ordinal) (_x : a < o), a)

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

### Fixed points of addition #

@[simp]
theorem ordinal.nfp_add_zero (a : ordinal) :
0 =
theorem ordinal.nfp_add_eq_mul_omega {a b : ordinal} (hba : b ) :
b =

### Fixed points of multiplication #

@[simp]
theorem ordinal.nfp_mul_one {a : ordinal} (ha : 0 < a) :
1 =
@[simp]
theorem ordinal.nfp_mul_zero (a : ordinal) :
0 = 0
@[simp]
theorem ordinal.nfp_zero_mul  :
@[simp]
theorem ordinal.nfp_mul_eq_opow_omega {a b : ordinal} (hb : 0 < b) (hba : b ) :
b =
theorem ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right {a b : ordinal} (hab : a * b = b) :
b = 0 b
theorem ordinal.mul_le_right_iff_opow_omega_dvd {a b : ordinal} (ha : 0 < a) :
a * b b b
theorem ordinal.nfp_mul_opow_omega_add {a c : ordinal} (b : ordinal) (ha : 0 < a) (hc : 0 < c) (hca : c ) :
* b + c) =
theorem ordinal.deriv_mul_eq_opow_omega_mul {a : ordinal} (ha : 0 < a) (b : ordinal) :
b = * b