mathlib3 documentation

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 #

Fixed points of type-indexed families of ordinals #

noncomputable def ordinal.nfp_family {ι : Type u} (f : ι ordinal ordinal) (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.foldr_le_nfp_family {ι : Type u} (f : ι ordinal ordinal) (a : ordinal) (l : list ι) :
theorem ordinal.lt_nfp_family {ι : Type u} {f : ι ordinal ordinal} {a b : ordinal} :
a < ordinal.nfp_family f b (l : list ι), a < list.foldr f b l
theorem ordinal.nfp_family_le_iff {ι : Type u} {f : ι ordinal ordinal} {a b : ordinal} :
ordinal.nfp_family f a b (l : list ι), list.foldr f a l b
theorem ordinal.nfp_family_le {ι : Type u} {f : ι ordinal ordinal} {a b : ordinal} :
( (l : list ι), list.foldr f a l b) ordinal.nfp_family f a b
theorem ordinal.nfp_family_monotone {ι : Type u} {f : ι ordinal ordinal} (hf : (i : ι), monotone (f i)) :
theorem ordinal.apply_lt_nfp_family {ι : Type u} {f : ι ordinal ordinal} (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} (hb : b < ordinal.nfp_family f a) (i : ι) :
theorem ordinal.apply_lt_nfp_family_iff {ι : Type u} {f : ι ordinal ordinal} [nonempty ι] (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
( (i : ι), f i b < ordinal.nfp_family f a) b < ordinal.nfp_family f a
theorem ordinal.nfp_family_le_apply {ι : Type u} {f : ι ordinal ordinal} [nonempty ι] (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
theorem ordinal.nfp_family_le_fp {ι : Type u} {f : ι ordinal ordinal} (H : (i : ι), monotone (f i)) {a b : ordinal} (ab : a b) (h : (i : ι), f i b b) :
theorem ordinal.nfp_family_fp {ι : Type u} {f : ι ordinal ordinal} {i : ι} (H : ordinal.is_normal (f i)) (a : ordinal) :
theorem ordinal.apply_le_nfp_family {ι : Type u} [hι : nonempty ι] {f : ι ordinal ordinal} (H : (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
( (i : ι), f i b ordinal.nfp_family f a) b ordinal.nfp_family f a
theorem ordinal.nfp_family_eq_self {ι : Type u} {f : ι ordinal ordinal} {a : ordinal} (h : (i : ι), f i a = a) :
theorem ordinal.fp_family_unbounded {ι : Type u} {f : ι ordinal ordinal} (H : (i : ι), ordinal.is_normal (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 : ι ordinal ordinal) (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
theorem ordinal.deriv_family_limit {ι : Type u} (f : ι ordinal ordinal) {o : ordinal} :
theorem ordinal.deriv_family_fp {ι : Type u} {f : ι ordinal ordinal} {i : ι} (H : ordinal.is_normal (f i)) (o : ordinal) :
theorem ordinal.le_iff_deriv_family {ι : Type u} {f : ι ordinal ordinal} (H : (i : ι), ordinal.is_normal (f i)) {a : ordinal} :
( (i : ι), f i a a) (o : ordinal), ordinal.deriv_family f o = a
theorem ordinal.fp_iff_deriv_family {ι : Type u} {f : ι ordinal ordinal} (H : (i : ι), ordinal.is_normal (f i)) {a : ordinal} :
( (i : ι), f i a = a) (o : ordinal), ordinal.deriv_family f o = a

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 ordinal ordinal) :

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.le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < o ordinal ordinal) (a : ordinal) :
theorem ordinal.lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} {a b : ordinal} :
theorem ordinal.nfp_bfamily_le {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} {a b : ordinal} :
theorem ordinal.nfp_bfamily_monotone {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} (hf : (i : ordinal) (hi : i < o), monotone (f i hi)) :
theorem ordinal.apply_lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} (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 ordinal ordinal} (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 ordinal ordinal} (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 ordinal ordinal} (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 ordinal ordinal} {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 ordinal ordinal} (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 ordinal ordinal} {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 ordinal ordinal} (H : (i : ordinal) (hi : i < o), ordinal.is_normal (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 ordinal ordinal) :

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_fp {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} {i : ordinal} {hi : i < o} (H : ordinal.is_normal (f i hi)) (a : ordinal) :
f i hi (o.deriv_bfamily f a) = o.deriv_bfamily f a
theorem ordinal.le_iff_deriv_bfamily {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} (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), o.deriv_bfamily f b = a
theorem ordinal.fp_iff_deriv_bfamily {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} (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), o.deriv_bfamily f b = a
theorem ordinal.deriv_bfamily_eq_enum_ord {o : ordinal} {f : Π (b : ordinal), b < o ordinal ordinal} (H : (i : ordinal) (hi : i < o), ordinal.is_normal (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)) = ordinal.nfp f
theorem ordinal.iterate_le_nfp (f : ordinal ordinal) (a : ordinal) (n : ) :
theorem ordinal.lt_nfp {f : ordinal ordinal} {a b : ordinal} :
a < ordinal.nfp f b (n : ), a < f^[n] b
theorem ordinal.nfp_le_iff {f : ordinal ordinal} {a b : ordinal} :
ordinal.nfp f a b (n : ), f^[n] a b
theorem ordinal.nfp_le {f : ordinal ordinal} {a b : ordinal} :
( (n : ), f^[n] a b) ordinal.nfp f a b
@[simp]
theorem ordinal.nfp_le_fp {f : ordinal ordinal} (H : monotone f) {a b : ordinal} (ab : a b) (h : f b b) :
theorem ordinal.nfp_eq_self {f : ordinal ordinal} {a : ordinal} (h : f 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
theorem ordinal.deriv_limit (f : ordinal ordinal) {o : ordinal} :
o.is_limit ordinal.deriv f o = o.bsup (λ (a : ordinal) (_x : a < o), ordinal.deriv f a)

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

Fixed points of addition #

Fixed points of multiplication #

@[simp]
theorem ordinal.nfp_mul_one {a : ordinal} (ha : 0 < a) :
@[simp]
theorem ordinal.nfp_mul_opow_omega_add {a c : ordinal} (b : ordinal) (ha : 0 < a) (hc : 0 < c) (hca : c a ^ ordinal.omega) :