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 #

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 : ι → 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

ordinal.nfp_family f a = ordinal.sup (list.foldr f a)

theorem ordinal.nfp_family_eq_sup {ι : Type u} (f : ι → ordinal → ordinal) (a : ordinal) :

ordinal.nfp_family f a = ordinal.sup (list.foldr f a)

theorem ordinal.foldr_le_nfp_family {ι : Type u} (f : ι → ordinal → ordinal) (a : ordinal) (l : list ι) :

list.foldr f a l ≤ ordinal.nfp_family f a

theorem ordinal.le_nfp_family {ι : Type u} (f : ι → ordinal → ordinal) (a : ordinal) :

a ≤ ordinal.nfp_family f a

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

monotone (ordinal.nfp_family f)

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

f i b < ordinal.nfp_family f a

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

(∃ (i : ι), ordinal.nfp_family f a ≤ f i b) ↔ ordinal.nfp_family f a ≤ b

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

ordinal.nfp_family f a ≤ b

theorem ordinal.nfp_family_fp {ι : Type u} {f : ι → ordinal → ordinal} {i : ι} (H : ordinal.is_normal (f i)) (a : ordinal) :

f i (ordinal.nfp_family f a) = ordinal.nfp_family f a

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

ordinal.nfp_family f a = a

theorem ordinal.fp_family_unbounded {ι : Type u} {f : ι → ordinal → ordinal} (H : ∀ (i : ι), ordinal.is_normal (f i)) :

set.unbounded has_lt.lt (⋂ (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 : ι → 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

ordinal.deriv_family f o = o.limit_rec_on (ordinal.nfp_family f 0) (λ (a IH : ordinal), ordinal.nfp_family f (order.succ IH)) (λ (a : ordinal) (l : a.is_limit), a.bsup)

@[simp]

theorem ordinal.deriv_family_zero {ι : Type u} (f : ι → ordinal → ordinal) :

ordinal.deriv_family f 0 = ordinal.nfp_family f 0

@[simp]

theorem ordinal.deriv_family_succ {ι : Type u} (f : ι → ordinal → ordinal) (o : ordinal) :

ordinal.deriv_family f (order.succ o) = ordinal.nfp_family f (order.succ (ordinal.deriv_family f o))

theorem ordinal.deriv_family_limit {ι : Type u} (f : ι → ordinal → ordinal) {o : ordinal} :

o.is_limit → ordinal.deriv_family f o = o.bsup (λ (a : ordinal) (_x : a < o), ordinal.deriv_family f a)

theorem ordinal.deriv_family_is_normal {ι : Type u} (f : ι → ordinal → ordinal) :

ordinal.is_normal (ordinal.deriv_family f)

theorem ordinal.deriv_family_fp {ι : Type u} {f : ι → ordinal → ordinal} {i : ι} (H : ordinal.is_normal (f i)) (o : ordinal) :

f i (ordinal.deriv_family f o) = ordinal.deriv_family f o

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

theorem ordinal.deriv_family_eq_enum_ord {ι : Type u} {f : ι → ordinal → ordinal} (H : ∀ (i : ι), ordinal.is_normal (f i)) :

ordinal.deriv_family f = ordinal.enum_ord (⋂ (i : ι), function.fixed_points (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 → ordinal → ordinal) :

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

o.nfp_bfamily f = ordinal.nfp_family (o.family_of_bfamily f)

theorem ordinal.nfp_bfamily_eq_nfp_family {o : ordinal} (f : Π (b : ordinal), b < o → ordinal → ordinal) :

o.nfp_bfamily f = ordinal.nfp_family (o.family_of_bfamily f)

theorem ordinal.foldr_le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < o → ordinal → ordinal) (a : ordinal) (l : list (quotient.out o).α) :

list.foldr (o.family_of_bfamily f) a l ≤ o.nfp_bfamily f a

theorem ordinal.le_nfp_bfamily {o : ordinal} (f : Π (b : ordinal), b < o → ordinal → ordinal) (a : ordinal) :

a ≤ o.nfp_bfamily f a

theorem ordinal.lt_nfp_bfamily {o : ordinal} {f : Π (b : ordinal), b < o → ordinal → ordinal} {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 < o → ordinal → ordinal} {a b : ordinal} :

o.nfp_bfamily f a ≤ b ↔ ∀ (l : list (quotient.out o).α), list.foldr (o.family_of_bfamily f) a l ≤ b

theorem ordinal.nfp_bfamily_le {o : ordinal} {f : Π (b : ordinal), b < o → ordinal → ordinal} {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 < o → ordinal → ordinal} (hf : ∀ (i : ordinal) (hi : i < o), monotone (f i hi)) :

monotone (o.nfp_bfamily f)

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

o.nfp_bfamily f a ≤ 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)) :

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

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

o.deriv_bfamily f = ordinal.deriv_family (o.family_of_bfamily f)

theorem ordinal.deriv_bfamily_eq_deriv_family {o : ordinal} (f : Π (b : ordinal), b < o → ordinal → ordinal) :

o.deriv_bfamily f = ordinal.deriv_family (o.family_of_bfamily f)

theorem ordinal.deriv_bfamily_is_normal {o : ordinal} (f : Π (b : ordinal), b < o → ordinal → ordinal) :

ordinal.is_normal (o.deriv_bfamily f)

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

o.deriv_bfamily f = 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) :

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

ordinal.nfp f = ordinal.nfp_family (λ (_x : unit), f)

theorem ordinal.nfp_eq_nfp_family (f : ordinal → ordinal) :

ordinal.nfp f = ordinal.nfp_family (λ (_x : unit), f)

@[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 : ℕ) :

f^[n] a ≤ ordinal.nfp f a

theorem ordinal.le_nfp (f : ordinal → ordinal) (a : ordinal) :

a ≤ ordinal.nfp f a

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

ordinal.nfp id = id

theorem ordinal.nfp_monotone {f : ordinal → ordinal} (hf : monotone f) :

monotone (ordinal.nfp f)

theorem ordinal.is_normal.apply_lt_nfp {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f b < ordinal.nfp f a ↔ b < ordinal.nfp f a

theorem ordinal.is_normal.nfp_le_apply {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

ordinal.nfp f a ≤ f b ↔ ordinal.nfp f a ≤ b

theorem ordinal.nfp_le_fp {f : ordinal → ordinal} (H : monotone f) {a b : ordinal} (ab : a ≤ b) (h : f b ≤ b) :

ordinal.nfp f a ≤ b

theorem ordinal.is_normal.nfp_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) (a : ordinal) :

f (ordinal.nfp f a) = ordinal.nfp f a

theorem ordinal.is_normal.apply_le_nfp {f : ordinal → ordinal} (H : ordinal.is_normal f) {a b : ordinal} :

f b ≤ ordinal.nfp f a ↔ b ≤ ordinal.nfp f a

theorem ordinal.nfp_eq_self {f : ordinal → ordinal} {a : ordinal} (h : f a = a) :

ordinal.nfp f a = a

theorem ordinal.fp_unbounded {f : ordinal → ordinal} (H : ordinal.is_normal f) :

set.unbounded has_lt.lt (function.fixed_points f)

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

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

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

ordinal.deriv f = ordinal.deriv_family (λ (_x : unit), f)

theorem ordinal.deriv_eq_deriv_family (f : ordinal → ordinal) :

ordinal.deriv f = ordinal.deriv_family (λ (_x : unit), f)

@[simp]

theorem ordinal.deriv_zero (f : ordinal → ordinal) :

ordinal.deriv f 0 = ordinal.nfp f 0

@[simp]

theorem ordinal.deriv_succ (f : ordinal → ordinal) (o : ordinal) :

ordinal.deriv f (order.succ o) = ordinal.nfp f (order.succ (ordinal.deriv f o))

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)

theorem ordinal.deriv_is_normal (f : ordinal → ordinal) :

ordinal.is_normal (ordinal.deriv f)

theorem ordinal.deriv_id_of_nfp_id {f : ordinal → ordinal} (h : ordinal.nfp f = id) :

ordinal.deriv f = id

theorem ordinal.is_normal.deriv_fp {f : ordinal → ordinal} (H : ordinal.is_normal f) (o : ordinal) :

f (ordinal.deriv f o) = ordinal.deriv f o

theorem ordinal.is_normal.le_iff_deriv {f : ordinal → ordinal} (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 : ordinal → ordinal} (H : ordinal.is_normal f) {a : ordinal} :

f a = a ↔ ∃ (o : ordinal), ordinal.deriv f o = a

theorem ordinal.deriv_eq_enum_ord {f : ordinal → ordinal} (H : ordinal.is_normal f) :

ordinal.deriv f = ordinal.enum_ord (function.fixed_points f)

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

theorem ordinal.deriv_eq_id_of_nfp_eq_id {f : ordinal → ordinal} (h : ordinal.nfp f = id) :

ordinal.deriv f = id

Fixed points of addition #

@[simp]

theorem ordinal.nfp_add_zero (a : ordinal) :

ordinal.nfp (has_add.add a) 0 = a * ordinal.omega

theorem ordinal.nfp_add_eq_mul_omega {a b : ordinal} (hba : b ≤ a * ordinal.omega) :

ordinal.nfp (has_add.add a) b = a * ordinal.omega

theorem ordinal.add_eq_right_iff_mul_omega_le {a b : ordinal} :

a + b = b ↔ a * ordinal.omega ≤ b

theorem ordinal.add_le_right_iff_mul_omega_le {a b : ordinal} :

a + b ≤ b ↔ a * ordinal.omega ≤ b

theorem ordinal.deriv_add_eq_mul_omega_add (a b : ordinal) :

ordinal.deriv (has_add.add a) b = a * ordinal.omega + b

Fixed points of multiplication #

@[simp]

theorem ordinal.nfp_mul_one {a : ordinal} (ha : 0 < a) :

ordinal.nfp (has_mul.mul a) 1 = a ^ ordinal.omega

@[simp]

theorem ordinal.nfp_mul_zero (a : ordinal) :

ordinal.nfp (has_mul.mul a) 0 = 0

@[simp]

theorem ordinal.nfp_zero_mul :

ordinal.nfp (has_mul.mul 0) = id

@[simp]

theorem ordinal.deriv_mul_zero :

ordinal.deriv (has_mul.mul 0) = id

theorem ordinal.nfp_mul_eq_opow_omega {a b : ordinal} (hb : 0 < b) (hba : b ≤ a ^ ordinal.omega) :

ordinal.nfp (has_mul.mul a) b = a ^ ordinal.omega

theorem ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right {a b : ordinal} (hab : a * b = b) :

b = 0 ∨ a ^ ordinal.omega ≤ b

theorem ordinal.mul_eq_right_iff_opow_omega_dvd {a b : ordinal} :

a * b = b ↔ a ^ ordinal.omega ∣ b

theorem ordinal.mul_le_right_iff_opow_omega_dvd {a b : ordinal} (ha : 0 < a) :

a * b ≤ b ↔ a ^ ordinal.omega ∣ b

theorem ordinal.nfp_mul_opow_omega_add {a c : ordinal} (b : ordinal) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ ordinal.omega) :

ordinal.nfp (has_mul.mul a) (a ^ ordinal.omega * b + c) = a ^ ordinal.omega * order.succ b

theorem ordinal.deriv_mul_eq_opow_omega_mul {a : ordinal} (ha : 0 < a) (b : ordinal) :

ordinal.deriv (has_mul.mul a) b = a ^ ordinal.omega * b