mathlib documentation

set_theory.ordinal.fixed_point

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 #

Fixed points of type-indexed families of ordinals #

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

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

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 : ι → ordinalordinal) (a : ordinal) :
theorem ordinal.foldr_le_nfp_family {ι : Type u} (f : ι → ordinalordinal) (a : ordinal) (l : list ι) :
theorem ordinal.le_nfp_family {ι : Type u} (f : ι → ordinalordinal) (a : ordinal) :
theorem ordinal.lt_nfp_family {ι : Type u} {f : ι → ordinalordinal} {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 : ι → ordinalordinal} {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 : ι → ordinalordinal} {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 : ι → ordinalordinal} (hf : ∀ (i : ι), monotone (f i)) :
theorem ordinal.apply_lt_nfp_family {ι : Type u} {f : ι → ordinalordinal} (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 : ι → ordinalordinal} [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 : ι → ordinalordinal} [nonempty ι] (H : ∀ (i : ι), ordinal.is_normal (f i)) {a b : ordinal} :
(∃ (i : ι), ordinal.nfp_family f a f i b) ordinal.nfp_family f a b
theorem ordinal.nfp_family_le_fp {ι : Type u} {f : ι → ordinalordinal} (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 : ι → ordinalordinal} {i : ι} (H : ordinal.is_normal (f i)) (a : ordinal) :
theorem ordinal.apply_le_nfp_family {ι : Type u} [hι : nonempty ι] {f : ι → ordinalordinal} (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 : ι → ordinalordinal} {a : ordinal} (h : ∀ (i : ι), f i a = a) :
theorem ordinal.fp_family_unbounded {ι : Type u} {f : ι → ordinalordinal} (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 : ι → ordinalordinal) (o : ordinal) :

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

Equations
@[simp]
theorem ordinal.deriv_family_zero {ι : Type u} (f : ι → ordinalordinal) :
theorem ordinal.deriv_family_limit {ι : Type u} (f : ι → ordinalordinal) {o : ordinal} :
o.is_limitordinal.deriv_family f o = o.bsup (λ (a : ordinal) (_x : a < o), ordinal.deriv_family f a)
theorem ordinal.deriv_family_fp {ι : Type u} {f : ι → ordinalordinal} {i : ι} (H : ordinal.is_normal (f i)) (o : ordinal) :
theorem ordinal.le_iff_deriv_family {ι : Type u} {f : ι → ordinalordinal} (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 : ι → ordinalordinal} (H : ∀ (i : ι), ordinal.is_normal (f i)) {a : ordinal} :
(∀ (i : ι), f i a = a) ∃ (o : ordinal), ordinal.deriv_family f o = a
theorem ordinal.deriv_family_eq_enum_ord {ι : Type u} {f : ι → ordinalordinal} (H : ∀ (i : ι), ordinal.is_normal (f i)) :

Fixed points of ordinal-indexed families of ordinals #

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

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

Equations
theorem ordinal.foldr_le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < oordinalordinal) (a : ordinal) (l : list (quotient.out o).α) :
theorem ordinal.le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < oordinalordinal) (a : ordinal) :
theorem ordinal.lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} {a b : ordinal} :
a < o.nfp_bfamily f b ∃ (l : list (quotient.out o).α), a < list.foldr (o.family_of_bfamily f) b l
theorem ordinal.nfp_bfamily_le_iff {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} {a b : ordinal} :
theorem ordinal.nfp_bfamily_le {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} {a b : ordinal} :
(∀ (l : list (quotient.out o).α), list.foldr (o.family_of_bfamily f) a l b)o.nfp_bfamily f a b
theorem ordinal.nfp_bfamily_monotone {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} (hf : ∀ (i : ordinal) (hi : i < o), monotone (f i hi)) :
theorem ordinal.apply_lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} (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 < oordinalordinal} (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 < oordinalordinal} (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 < oordinalordinal} {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 < oordinalordinal} (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 < oordinalordinal} {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 < oordinalordinal} (H : ∀ (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) :
set.unbounded has_lt.lt (⋂ (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 < oordinalordinal) :

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

Equations
theorem ordinal.deriv_bfamily_fp {o : ordinal} {f : Π (b : ordinal), b < oordinalordinal} {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 < oordinalordinal} (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 < oordinalordinal} (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 < oordinalordinal} (H : ∀ (i : ordinal) (hi : i < o), ordinal.is_normal (f i hi)) :
o.deriv_bfamily f = ordinal.enum_ord (⋂ (i : ordinal) (hi : i < o), function.fixed_points (f i hi))

Fixed points of a single function #

noncomputable def ordinal.nfp (f : ordinalordinal) :

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

Equations
@[simp]
theorem ordinal.sup_iterate_eq_nfp (f : ordinalordinal) :
(λ (a : ordinal), ordinal.sup (λ (n : ), f^[n] a)) = ordinal.nfp f
theorem ordinal.iterate_le_nfp (f : ordinalordinal) (a : ordinal) (n : ) :
theorem ordinal.le_nfp (f : ordinalordinal) (a : ordinal) :
theorem ordinal.lt_nfp {f : ordinalordinal} {a b : ordinal} :
a < ordinal.nfp f b ∃ (n : ), a < f^[n] b
theorem ordinal.nfp_le_iff {f : ordinalordinal} {a b : ordinal} :
ordinal.nfp f a b ∀ (n : ), f^[n] a b
theorem ordinal.nfp_le {f : ordinalordinal} {a b : ordinal} :
(∀ (n : ), f^[n] a b)ordinal.nfp f a b
@[simp]
theorem ordinal.nfp_le_fp {f : ordinalordinal} (H : monotone f) {a b : ordinal} (ab : a b) (h : f b b) :
theorem ordinal.nfp_eq_self {f : ordinalordinal} {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 : ordinalordinal) :

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

Equations
@[simp]
theorem ordinal.deriv_limit (f : ordinalordinal) {o : ordinal} :
o.is_limitordinal.deriv f o = o.bsup (λ (a : ordinal) (_x : a < o), ordinal.deriv f a)
theorem ordinal.is_normal.le_iff_deriv {f : ordinalordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a a ∃ (o : ordinal), ordinal.deriv f o = a
theorem ordinal.is_normal.fp_iff_deriv {f : ordinalordinal} (H : ordinal.is_normal f) {a : ordinal} :
f a = a ∃ (o : ordinal), ordinal.deriv f o = a

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