Ordinal.le_nfpFamily
theorem Ordinal.le_nfpFamily :
∀ {ι : Type u} (f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}) (a : Ordinal.{max u u_1}),
a ≤ Ordinal.nfpFamily f a
The theorem `Ordinal.le_nfpFamily` states that for any type `ι`, any function `f` mapping `ι` and an ordinal to an ordinal, and any ordinal `a`, the ordinal `a` is less than or equal to the next common fixed point of `f` starting from `a`. Here, "next common fixed point" refers to the supremum of all values reachable by applying finitely many functions in the family to `a`.
More concisely: For any type `ι`, function `f` mapping `ι` to ordinals, and ordinal `a`, the ordinal `a` is less than or equal to the supremum of all ordinals reachable from `a` through finitely many applications of `f`.
|
Ordinal.derivBFamily_eq_enumOrd
theorem Ordinal.derivBFamily_eq_enumOrd :
∀ {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}},
(∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) →
o.derivBFamily f = Ordinal.enumOrd (⋂ i, ⋂ (hi : i < o), Function.fixedPoints (f i hi))
This theorem states that for a family of ordinal functions, where each function is "normal" (i.e., it is strictly increasing and the image of a limit ordinal is the sup of the function values for all lesser ordinals), the `Ordinal.derivBFamily` function, which enumerates these functions, is equivalent to the `Ordinal.enumOrd` function over the intersection of all fixed points of the given normal functions. In other words, the common fixed points of these normal functions are exactly those enumerated by `Ordinal.derivBFamily`.
More concisely: For a family of normal ordinal functions, the functions enumerated by `Ordinal.derivBFamily` are exactly the common fixed points of these functions, which is equal to the ordinals enumerated by `Ordinal.enumOrd` over their intersection.
|
Ordinal.derivFamily_fp
theorem Ordinal.derivFamily_fp :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {i : ι},
Ordinal.IsNormal (f i) → ∀ (o : Ordinal.{max u v}), f i (Ordinal.derivFamily f o) = Ordinal.derivFamily f o
This theorem states that for any type `ι`, any function `f` from `ι` and an ordinal to an ordinal, and any element `i` of type `ι`, if `f i` is a normal ordinal function, then for any ordinal `o`, applying `f i` to the derivative of the family `f` at `o` results in the derivative of the family `f` at `o` itself. In other words, the derivative of the family `f` at `o` is a fixed point of the function `f i` when `f i` is a normal ordinal function.
More concisely: For any function `f` from a type `ι` to ordinal numbers, and any `i` in `ι` such that `f i` is a normal ordinal function, the derivative of `f` at an ordinal `o` is equal to `f i` applied to the derivative of `f` at `o`.
|
Ordinal.deriv_isNormal
theorem Ordinal.deriv_isNormal : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.IsNormal (Ordinal.deriv f)
The theorem `Ordinal.deriv_isNormal` states that for every ordinal function `f`, the derivative of `f` is a normal function. In other words, the derivative of any ordinal function is a strictly increasing function that is order-continuous. In mathematical terms, if `f` is an ordinal function, then its derivative `f'` satisfies the conditions: `f'(o) < f'(o+1)` for all ordinals `o`, and for any limit ordinal `o` and any ordinal `a`, `f'(o) ≤ a` if and only if `f'(b) ≤ a` for all `b < o`.
More concisely: The derivative of every ordinal function is a strictly increasing and order-continuous function.
|
Ordinal.fp_unbounded
theorem Ordinal.fp_unbounded :
∀ {f : Ordinal.{u} → Ordinal.{u}},
Ordinal.IsNormal f → Set.Unbounded (fun x x_1 => x < x_1) (Function.fixedPoints f)
The theorem `Ordinal.fp_unbounded` is referred to as the "Fixed Point Lemma for Normal Functions". It states that for any normal function `f`, which is a strictly increasing function that maps a limit ordinal to the supremum of its function values on smaller ordinals, there exists an unbounded or cofinal set of fixed points. In other words, for any ordinal `x`, there is a fixed point `y` of the function `f` such that `x < y`. This means that no matter how large an ordinal we choose, we can always find a fixed point that is larger, implying that the set of fixed points is unbounded.
More concisely: For any normal function mapping limit ordinals to their supremum over smaller ordinals, there exists an unbounded set of fixed points.
|
Ordinal.deriv_zero
theorem Ordinal.deriv_zero : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.deriv f 0 = Ordinal.nfp f 0
This theorem, `Ordinal.deriv_zero`, states that for any ordinal function `f` that maps an ordinal to another ordinal, the derivative of `f` at zero equals the least fixed point of `f` at zero. In other words, the first fixed point of a normal function `f` that does not fall below zero is the derivative of `f` at zero. This establishes a fundamental relationship between the derivative and the least fixed point of an ordinal function at zero.
More concisely: The derivative of an ordinal function at zero equals its least fixed point at zero.
|
Ordinal.nfp_le_fp
theorem Ordinal.nfp_le_fp :
∀ {f : Ordinal.{u_1} → Ordinal.{u_1}},
Monotone f → ∀ {a b : Ordinal.{u_1}}, a ≤ b → f b ≤ b → Ordinal.nfp f a ≤ b
The theorem `Ordinal.nfp_le_fp` states that for all functions `f` from an ordinal to an ordinal, if `f` is monotone, then for all ordinals `a` and `b`, if `a` is less than or equal to `b` and `f` of `b` is less than or equal to `b`, then the least fixed point of `f` that is at least `a` is less than or equal to `b`. In other words, for a monotone function `f` on ordinals, the least fixed point of `f` that is at least `a`, does not exceed `b` under the conditions that `a` does not exceed `b` and the value of `f` at `b` does not exceed `b`.
More concisely: For any monotonic function f from ordinals to ordinals, if a ≤ b and f(b) ≤ b hold, then the least fixed point of f above a is less than or equal to b.
|
Ordinal.nfp_add_zero
theorem Ordinal.nfp_add_zero : ∀ (a : Ordinal.{u_1}), Ordinal.nfp (fun x => a + x) 0 = a * Ordinal.omega
The theorem `Ordinal.nfp_add_zero` states that for any ordinal `a`, the least fixed point of the function `f(x) = a + x`, starting at 0, is equal to `a` times the first infinite ordinal `ω`. In other words, when you repeatedly apply the function `f(x) = a + x` starting at 0 until reaching a fixed point, you will arrive at the product of `a` and `ω`, where `ω` is the order type of the set of natural numbers.
More concisely: The least fixed point of the function `a +` is equal to `a * ω`, where `a` is an ordinal and `ω` is the first infinite ordinal.
|
Ordinal.derivFamily_succ
theorem Ordinal.derivFamily_succ :
∀ {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v}) (o : Ordinal.{max u v}),
Ordinal.derivFamily f (Order.succ o) = Ordinal.nfpFamily f (Order.succ (Ordinal.derivFamily f o))
This theorem states that for any type `ι` and function `f` from `ι` to an ordinal, and for any ordinal `o`, the derivative of `f` at the successor of `o` is equal to the next common fixed point of `f` at the successor of the derivative of `f` at `o`. In simpler terms, it relates the concepts of derivatives and successors in the context of ordinal arithmetic and normal function families. The theorem provides an important property concerning the interplay between the operation of taking derivatives and successors within the specific mathematical structure of ordinals and normal functions.
More concisely: For any type `ι`, function `f` from `ι` to an ordinal, and ordinal `o`, the derivative of `f` at the successor of `o` is equal to the next common fixed point of `f` at the successor of the derivative of `f` at `o`.
|
Ordinal.derivFamily_eq_enumOrd
theorem Ordinal.derivFamily_eq_enumOrd :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}},
(∀ (i : ι), Ordinal.IsNormal (f i)) → Ordinal.derivFamily f = Ordinal.enumOrd (⋂ i, Function.fixedPoints (f i))
The theorem `Ordinal.derivFamily_eq_enumOrd` states that for any type `ι` and a family of normal functions `f` mapping from `ι` to ordinals, if every function in the family `f` is a normal function (i.e., it is strictly increasing and order-continuous), then the derivative of this family of functions, given by `Ordinal.derivFamily f`, is equivalent to enumerating the common fixed points of the functions in the family. Here, a fixed point of a function is an element that is mapped to itself by the function. The common fixed points of a family of functions are those elements that are fixed points for every function in the family.
More concisely: Given a type `ι` and a family of normal functions `f` from `ι` to ordinals, the derivative of `f` is equal to the enumeration of their common fixed points.
|
Ordinal.sup_iterate_eq_nfp
theorem Ordinal.sup_iterate_eq_nfp :
∀ (f : Ordinal.{u} → Ordinal.{u}), (fun a => Ordinal.sup fun n => f^[n] a) = Ordinal.nfp f
The theorem `Ordinal.sup_iterate_eq_nfp` asserts that for any function `f` from an ordinal to an ordinal, the function that takes an ordinal `a` to the supremum of the sequence formed by iteratively applying `f` to `a` is equivalent to the next fixed point function of `f`. In more mathematical terms, if `f` is a function from an ordinal to an ordinal, then the function that maps `a` to the supremum of the sequence `{f^n(a) | n ∈ ℕ}` is the same as the least fixed point of `f` that is greater than or equal to `a`.
More concisely: For any ordinal-valued function `f`, the supremum of the iterated sequence `{f^n(a) | n ∈ ℕ}` equals the least fixed point of `f` greater than or equal to `a`.
|
Ordinal.deriv_succ
theorem Ordinal.deriv_succ :
∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}),
Ordinal.deriv f (Order.succ o) = Ordinal.nfp f (Order.succ (Ordinal.deriv f o))
The theorem `Ordinal.deriv_succ` states that for any normal function `f` from an ordinal to another ordinal, and for any ordinal `o`, the derivative of `f` at the successor of `o` is equal to the next fixed point of `f` at the successor of the derivative of `f` at `o`. In other words, it formalizes the relationship between the derivative of a normal function at a certain point and the next fixed point of the function at a related point.
More concisely: For any normal function from an ordinal to an ordinal, the derivative at the successor of an ordinal is the next fixed point at the successor of the derivative.
|
Ordinal.derivFamily_zero
theorem Ordinal.derivFamily_zero :
∀ {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v}), Ordinal.derivFamily f 0 = Ordinal.nfpFamily f 0
This theorem states that for any type `ι` and any family of functions `f` from `ι` to the ordinals, the derivative of the family of functions at 0 is equal to the next common fixed point of the family of functions at 0. In other words, if you have a collection of functions (indexed by `ι`) that take ordinals to ordinals, then if you apply the derivative operator to this family at the ordinal 0, you get the same ordinal as if you had computed the next common fixed point of the family at 0.
More concisely: For any type `ι` and family of ordinal-valued functions `f` from `ι` to ordinals, the derivative of `f` at 0 is equal to the next common fixed point of `f` at 0.
|
Ordinal.nfpFamily_fp
theorem Ordinal.nfpFamily_fp :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {i : ι},
Ordinal.IsNormal (f i) → ∀ (a : Ordinal.{max u v}), f i (Ordinal.nfpFamily f a) = Ordinal.nfpFamily f a
The theorem `Ordinal.nfpFamily_fp` states that for any type `ι`, any function `f` from `ι` to a normal ordinal function, and any `i` of type `ι`, if `f i` is a normal ordinal function then for any ordinal `a`, applying `f i` to the next common fixed point of the family (at least `a`) gives you the next common fixed point itself. In simpler terms, the next common fixed point is a fixed point for each of the normal functions in the family.
More concisely: For any type `ι`, function `f` from `ι` to normal ordinal functions, and `i` of type `ι`, if `f i` is a normal ordinal function and `a` is the next common fixed point of the family `(f i)` (or greater), then `(f i) (next_cpp a) = next_cpp a`.
|
Ordinal.derivFamily_isNormal
theorem Ordinal.derivFamily_isNormal :
∀ {ι : Type u} (f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}), Ordinal.IsNormal (Ordinal.derivFamily f) := by
sorry
The theorem `Ordinal.derivFamily_isNormal` states that for all types `ι` and for any function `f` from `ι` to a family of ordinals, the derivative family of `f`, which is represented as `Ordinal.derivFamily f`, is a normal ordinal function. A normal ordinal function, in this context, means that the function is strictly increasing and order-continuous. This implies that the image of a limit ordinal under this function is the supremum of the images of the ordinals less than the original limit ordinal.
More concisely: The derivative family of a function from an type `ι` to ordinals is a normal ordinal function, i.e., it is strictly increasing and order-continuous, ensuring the image of a limit ordinal is the supremum of the images of smaller ordinals.
|
Ordinal.nfpFamily_le_fp
theorem Ordinal.nfpFamily_le_fp :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}},
(∀ (i : ι), Monotone (f i)) →
∀ {a b : Ordinal.{max u v}}, a ≤ b → (∀ (i : ι), f i b ≤ b) → Ordinal.nfpFamily f a ≤ b
The theorem `Ordinal.nfpFamily_le_fp` states that for any type `ι` and a function `f` from `ι` to a mapping from an ordinal to another ordinal, if every `f i` is a monotone function, then for any two ordinals `a` and `b` where `a` is less than or equal to `b`, and for every `i` in `ι`, `f i b` is less than or equal to `b`, it follows that the next common fixed point for the family of functions `f`, starting at least `a`, is less than or equal to `b`. In short, it states that the least ordinal fixed point for a family of monotone functions is bounded.
More concisely: For any type `ι` and a family `f` of monotone functions from `ι` to ordinals, if for all `i` in `ι` and ordinals `a` and `b` with `a ≤ b`, we have `f i b ≤ b`, then the least fixed point of `f` is less than or equal to `b`.
|
Ordinal.apply_lt_nfpFamily_iff
theorem Ordinal.apply_lt_nfpFamily_iff :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} [inst : Nonempty ι],
(∀ (i : ι), Ordinal.IsNormal (f i)) →
∀ {a b : Ordinal.{max u v}}, (∀ (i : ι), f i b < Ordinal.nfpFamily f a) ↔ b < Ordinal.nfpFamily f a
The theorem `Ordinal.apply_lt_nfpFamily_iff` states that for any type `ι`, any function `f` from `ι` to the set of ordinals, and any two ordinals `a` and `b`, as long as `ι` is nonempty and every function `f i` is a normal ordinal function, then for all `i` in `ι`, `f i b` is less than the next common fixed point at least `a` for the family of functions if and only if `b` is less than the next common fixed point at least `a` for the family of functions. In other words, the property of `b` being less than the next common fixed point is equivalent to the property of the image of `b` under all the functions being less than this next common fixed point.
More concisely: For any nonempty type `ι` and normal ordinal function `f` from `ι` to ordinals, `b` is less than the next common fixed point at least `a` for `f` if and only if `f i b` is less than the next common fixed point for all `i` in `ι`.
|
Ordinal.fp_family_unbounded
theorem Ordinal.fp_family_unbounded :
∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}},
(∀ (i : ι), Ordinal.IsNormal (f i)) → Set.Unbounded (fun x x_1 => x < x_1) (⋂ i, Function.fixedPoints (f i))
The theorem `Ordinal.fp_family_unbounded` is a generalization of the fixed point lemma for normal functions. It states that for any family of normal functions, indexed by a type `ι`, where each function maps an ordinal of a certain type to an ordinal of the same type, there exists an unbounded set of common fixed points. In other words, given any ordinal `x`, there exists an ordinal `x_1` in the intersection of the fixed points of all functions such that `x < x_1`. Here, a function is normal if it is strictly increasing and order-continuous. A set is unbounded if for any element, there exists another element in the set that is not less than the given element. A fixed point of a function is an element that is left unchanged by the function.
More concisely: For any normal family of functions from ordinals to ordinals indexed by type ι, there exists an unbounded set of common fixed points.
|
Ordinal.fp_bfamily_unbounded
theorem Ordinal.fp_bfamily_unbounded :
∀ {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}},
(∀ (i : Ordinal.{u}) (hi : i < o), Ordinal.IsNormal (f i hi)) →
Set.Unbounded (fun x x_1 => x < x_1) (⋂ i, ⋂ (hi : i < o), Function.fixedPoints (f i hi))
This theorem, referred to as the "fixed point lemma for normal functions", is a generalization of a similar lemma for single functions. It states that given any family of normal functions indexed by an ordinal less than a given ordinal 'o', where each function maps an ordinal to another ordinal, if each function is normal (meaning it is strictly increasing and order-continuous), then the intersection of the fixed points of these functions represents an unbounded set with respect to the order '<'. In other words, for any element in the ordinal universe, there exists an element in this intersection of fixed points that is greater than it. This means that there is no upper bound for the common fixed points of this family of normal functions.
More concisely: Given any family of normal functions indexed by an ordinal less than a given ordinal 'o', the intersection of their fixed points is an unbounded set with respect to the order '<'.
|
Ordinal.deriv_eq_enumOrd
theorem Ordinal.deriv_eq_enumOrd :
∀ {f : Ordinal.{u} → Ordinal.{u}},
Ordinal.IsNormal f → Ordinal.deriv f = Ordinal.enumOrd (Function.fixedPoints f)
The theorem `Ordinal.deriv_eq_enumOrd` states that for any normal function `f` that operates on ordinals, its derivative as defined by `Ordinal.deriv` is equivalent to enumerating its fixed points using `Ordinal.enumOrd` applied to the fixed points of the function `f`. In other words, the sequence of fixed points of a normal function `f` (its derivative) can be obtained by enumerating the fixed points of that function. This establishes a connection between the derivative of a normal function and the enumeration of its fixed points.
More concisely: The derivative of a normal function on ordinals, as defined in Lean's `Ordinal.deriv`, is equivalent to the enumeration of its fixed points using `Ordinal.enumOrd`.
|
Ordinal.derivFamily_limit
theorem Ordinal.derivFamily_limit :
∀ {ι : Type u} (f : ι → Ordinal.{max u v} → Ordinal.{max u v}) {o : Ordinal.{max u v}},
o.IsLimit → Ordinal.derivFamily f o = o.bsup fun a x => Ordinal.derivFamily f a
The theorem `Ordinal.derivFamily_limit` states that for any type `ι` and any function `f` from `ι` and `Ordinal.{max u v}` to `Ordinal.{max u v}`, and for any limit ordinal `o`, the derivative of the family of normal functions at `o` is equal to the supremum of the family of ordinals indexed by the set of ordinals less than `o`, where each ordinal in this family is the derivative of the family of normal functions at that ordinal. In other words, this theorem describes a property of limit ordinals in the context of derivatives of families of normal functions.
More concisely: The derivative of the family of normal functions at a limit ordinal is the supremum of the derivatives of the family at all ordinals less than it.
|