doc-next-gen

Mathlib.SetTheory.Ordinal.FixedPoint

Module docstring

{"# 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

  • nfpFamily, nfp: the next fixed point of a (family of) normal function(s).
  • not_bddAbove_fp_family, not_bddAbove_fp: the (common) fixed points of a (family of) normal function(s) are unbounded in the ordinals.
  • deriv_add_eq_mul_omega0_add: a characterization of the derivative of addition.
  • deriv_mul_eq_opow_omega0_mul: a characterization of the derivative of multiplication. ","### Fixed points of type-indexed families of ordinals ","### Fixed points of a single function ","### Fixed points of addition ","### Fixed points of multiplication "}
Ordinal.nfpFamily definition
(f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : Ordinal
Full source 
/-- 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.nfpFamily_fp` shows this is a fixed point, `Ordinal.le_nfpFamily` shows it's at
least `a`, and `Ordinal.nfpFamily_le_fp` shows this is the least ordinal with these properties. -/
def nfpFamily (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) (a : OrdinalOrdinal.{u}) : Ordinal :=
  ⨆ i, List.foldr f a i
Next common fixed point of a family of ordinal functions
Informal description
Given a family of functions \( f : \iota \to \text{Ordinal} \to \text{Ordinal} \) and an ordinal \( a \), the term \( \text{nfpFamily}\, f\, a \) denotes the next common fixed point of the family \( f \) that is at least \( a \). It is defined as the supremum of all ordinals obtained by applying finite compositions of functions from \( f \) to \( a \), i.e., \( \text{nfpFamily}\, f\, a = \bigsqcup_{l \in \text{List}\, \iota} \text{foldr}\, f\, a\, l \).
Ordinal.foldr_le_nfpFamily theorem
[Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a l) : List.foldr f a l ≤ nfpFamily f a
Full source 
theorem foldr_le_nfpFamily [Small.{u} ι] (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) (a l) :
    List.foldr f a l ≤ nfpFamily f a :=
  Ordinal.le_iSup _ _
Folding Bound for Next Common Fixed Point of Ordinal Function Family
Informal description
For any $u$-small type $\iota$ and any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$, given an ordinal $a$ and a list $l$ of elements of $\iota$, the ordinal obtained by folding $f$ over $l$ starting from $a$ is less than or equal to the next common fixed point $\text{nfpFamily}\, f\, a$ of the family $f$ above $a$.
Ordinal.le_nfpFamily theorem
[Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a) : a ≤ nfpFamily f a
Full source 
theorem le_nfpFamily [Small.{u} ι] (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) (a) : a ≤ nfpFamily f a :=
  foldr_le_nfpFamily f a []
Lower Bound for Next Common Fixed Point of Ordinal Function Family
Informal description
For any $u$-small type $\iota$ and any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$, the next common fixed point $\text{nfpFamily}\, f\, a$ of the family $f$ above an ordinal $a$ satisfies $a \leq \text{nfpFamily}\, f\, a$.
Ordinal.lt_nfpFamily_iff theorem
[Small.{u} ι] {a b} : a < nfpFamily f b ↔ ∃ l, a < List.foldr f b l
Full source 
theorem lt_nfpFamily_iff [Small.{u} ι] {a b} : a < nfpFamily f b ↔ ∃ l, a < List.foldr f b l :=
  Ordinal.lt_iSup_iff
Characterization of ordinals below the next common fixed point of a family of ordinal functions
Informal description
Let $\iota$ be a $u$-small type and $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ be a family of ordinal functions. For ordinals $a$ and $b$, we have $a < \text{nfpFamily}\, f\, b$ if and only if there exists a finite composition $l$ of functions from $f$ such that $a < \text{foldr}\, f\, b\, l$.
Ordinal.nfpFamily_le_iff theorem
[Small.{u} ι] {a b} : nfpFamily f a ≤ b ↔ ∀ l, List.foldr f a l ≤ b
Full source 
theorem nfpFamily_le_iff [Small.{u} ι] {a b} : nfpFamilynfpFamily f a ≤ b ↔ ∀ l, List.foldr f a l ≤ b :=
  Ordinal.iSup_le_iff
Characterization of Upper Bound for Next Common Fixed Point of a Family of Ordinal Functions
Informal description
For a family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ indexed by a $u$-small type $\iota$, and for ordinals $a$ and $b$, the next common fixed point $\text{nfpFamily}\, f\, a$ is less than or equal to $b$ if and only if for every finite composition $l$ of functions from $f$, the result of applying $l$ to $a$ is less than or equal to $b$. In other words: \[ \text{nfpFamily}\, f\, a \leq b \leftrightarrow \forall l, \text{List.foldr}\, f\, a\, l \leq b \]
Ordinal.nfpFamily_le theorem
{a b} : (∀ l, List.foldr f a l ≤ b) → nfpFamily f a ≤ b
Full source 
theorem nfpFamily_le {a b} : (∀ l, List.foldr f a l ≤ b) → nfpFamily f a ≤ b :=
  Ordinal.iSup_le
Upper Bound Condition for Next Common Fixed Point of a Family of Ordinal Functions
Informal description
For any ordinals $a$ and $b$, if for every finite composition $l$ of functions from the family $f$, the result of applying $l$ to $a$ is less than or equal to $b$, then the next common fixed point of $f$ above $a$ is also less than or equal to $b$.
Ordinal.nfpFamily_monotone theorem
[Small.{u} ι] (hf : ∀ i, Monotone (f i)) : Monotone (nfpFamily f)
Full source 
theorem nfpFamily_monotone [Small.{u} ι] (hf : ∀ i, Monotone (f i)) : Monotone (nfpFamily f) :=
  fun _ _ h ↦ nfpFamily_le <| fun l ↦ (List.foldr_monotone hf l h).trans (foldr_le_nfpFamily _ _ l)
Monotonicity of Next Common Fixed Point for a Family of Ordinal Functions
Informal description
For any $u$-small type $\iota$ and any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ where each $f_i$ is monotone, the function $\text{nfpFamily}\, f$ is also monotone. That is, for any ordinals $a \leq b$, we have $\text{nfpFamily}\, f\, a \leq \text{nfpFamily}\, f\, b$.
Ordinal.apply_lt_nfpFamily theorem
[Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} (hb : b < nfpFamily f a) (i) : f i b < nfpFamily f a
Full source 
theorem apply_lt_nfpFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b}
    (hb : b < nfpFamily f a) (i) : f i b < nfpFamily f a :=
  let ⟨l, hl⟩ := lt_nfpFamily_iff.1 hb
  lt_nfpFamily_iff.2 ⟨i::l, (H i).strictMono hl⟩
Normal Functions Preserve Order Below Next Common Fixed Point
Informal description
Let $\iota$ be a $u$-small type and $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ be a family of normal ordinal functions. For any ordinals $a$ and $b$ with $b < \text{nfpFamily}\, f\, a$ and any index $i \in \iota$, we have $f_i(b) < \text{nfpFamily}\, f\, a$.
Ordinal.apply_lt_nfpFamily_iff theorem
[Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} : (∀ i, f i b < nfpFamily f a) ↔ b < nfpFamily f a
Full source 
theorem apply_lt_nfpFamily_iff [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b < nfpFamily f a) ↔ b < nfpFamily f a := by
  refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩
  let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))
  exact lt_nfpFamily_iff.2 <| ⟨l, (H _).le_apply.trans_lt hl⟩
Characterization of ordinals below the next common fixed point of a family of normal functions
Informal description
Let $\iota$ be a nonempty $u$-small type and $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ be a family of normal ordinal functions. For any ordinals $a$ and $b$, the following are equivalent: 1. For every $i \in \iota$, $f_i(b) < \text{nfpFamily}\, f\, a$. 2. $b < \text{nfpFamily}\, f\, a$.
Ordinal.nfpFamily_le_apply theorem
[Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} : (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b
Full source 
theorem nfpFamily_le_apply [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b := by
  rw [← not_iff_not]
  push_neg
  exact apply_lt_nfpFamily_iff H
Characterization of ordinals above the next common fixed point of a family of normal functions
Informal description
Let $\iota$ be a nonempty $u$-small type and $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ be a family of normal ordinal functions. For any ordinals $a$ and $b$, the following are equivalent: 1. There exists an index $i \in \iota$ such that $\text{nfpFamily}\, f\, a \leq f_i(b)$. 2. $\text{nfpFamily}\, f\, a \leq b$.
Ordinal.nfpFamily_le_fp theorem
(H : ∀ i, Monotone (f i)) {a b} (ab : a ≤ b) (h : ∀ i, f i b ≤ b) : nfpFamily f a ≤ b
Full source 
theorem nfpFamily_le_fp (H : ∀ i, Monotone (f i)) {a b} (ab : a ≤ b) (h : ∀ i, f i b ≤ b) :
    nfpFamily f a ≤ b := by
  apply Ordinal.iSup_le
  intro l
  induction' l with i l IH generalizing a
  · exact ab
  · exact (H i (IH ab)).trans (h i)
Upper bound for next common fixed point of monotone ordinal functions
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of monotone ordinal functions, and let $a, b$ be ordinals such that $a \leq b$. If for every $i \in \iota$ we have $f_i(b) \leq b$, then the next common fixed point of the family $\{f_i\}$ above $a$ satisfies $\text{nfpFamily}\, f\, a \leq b$.
Ordinal.nfpFamily_fp theorem
[Small.{u} ι] {i} (H : IsNormal (f i)) (a) : f i (nfpFamily f a) = nfpFamily f a
Full source 
theorem nfpFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (a) :
    f i (nfpFamily f a) = nfpFamily f a := by
  rw [nfpFamily, H.map_iSup]
  apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_
  · exact Ordinal.le_iSup _ (i::l)
  · exact H.le_apply.trans (Ordinal.le_iSup _ _)
Fixed Point Property of Next Common Fixed Point for Normal Ordinal Functions
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a $u$-small type $\iota$. For any $i \in \iota$ and any ordinal $a$, the function $f_i$ evaluated at the next common fixed point $\text{nfpFamily}\, f\, a$ equals $\text{nfpFamily}\, f\, a$, i.e., $f_i(\text{nfpFamily}\, f\, a) = \text{nfpFamily}\, f\, a$.
Ordinal.apply_le_nfpFamily theorem
[Small.{u} ι] [hι : Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} : (∀ i, f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a
Full source 
theorem apply_le_nfpFamily [Small.{u} ι] [hι : Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a := by
  refine ⟨fun h => ?_, fun h i => ?_⟩
  · obtain ⟨i⟩ := hι
    exact (H i).le_apply.trans (h i)
  · rw [← nfpFamily_fp (H i)]
    exact (H i).monotone h
Characterization of Bounds on Next Common Fixed Point for Normal Ordinal Functions
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a $u$-small type $\iota$, with $\iota$ nonempty. For any ordinals $a$ and $b$, the following are equivalent: 1. For every $i \in \iota$, $f_i(b) \leq \text{nfpFamily}\, f\, a$. 2. $b \leq \text{nfpFamily}\, f\, a$. Here, $\text{nfpFamily}\, f\, a$ denotes the next common fixed point of the family $\{f_i\}$ that is at least $a$.
Ordinal.nfpFamily_eq_self theorem
[Small.{u} ι] {a} (h : ∀ i, f i a = a) : nfpFamily f a = a
Full source 
theorem nfpFamily_eq_self [Small.{u} ι] {a} (h : ∀ i, f i a = a) : nfpFamily f a = a := by
  apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)
  intro l
  rw [List.foldr_fixed' h l]
Fixed Point Property of $\text{nfpFamily}$ for Common Fixed Points
Informal description
For any $u$-small type $\iota$ and any ordinal $a$, if $a$ is a common fixed point of the family of functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ (i.e., $f_i(a) = a$ for all $i \in \iota$), then the next common fixed point $\text{nfpFamily}\, f\, a$ equals $a$.
Ordinal.not_bddAbove_fp_family theorem
[Small.{u} ι] (H : ∀ i, IsNormal (f i)) : ¬BddAbove (⋂ i, Function.fixedPoints (f i))
Full source 
/-- A generalization of the fixed point lemma for normal functions: any family of normal functions
    has an unbounded set of common fixed points. -/
theorem not_bddAbove_fp_family [Small.{u} ι] (H : ∀ i, IsNormal (f i)) :
    ¬ BddAbove (⋂ i, Function.fixedPoints (f i)) := by
  rw [not_bddAbove_iff]
  refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
  rintro _ ⟨i, rfl⟩
  exact nfpFamily_fp (H i) _
Unboundedness of Common Fixed Points for Normal Ordinal Functions
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a small type $\iota$. Then the set of common fixed points $\bigcap_i \{x \mid f_i(x) = x\}$ is unbounded in the ordinals. In other words, for any ordinal $\alpha$, there exists a common fixed point $\beta \geq \alpha$ such that $f_i(\beta) = \beta$ for all $i \in \iota$.
Ordinal.derivFamily definition
(f : ι → Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u}
Full source 
/-- 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.derivFamily_zero`,
`Ordinal.derivFamily_succ`, and `Ordinal.derivFamily_limit` are satisfied. -/
def derivFamily (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) (o : OrdinalOrdinal.{u}) : OrdinalOrdinal.{u} :=
  limitRecOn o (nfpFamily f 0) (fun _ IH => nfpFamily f (succ IH))
    fun a _ g => ⨆ b : Set.Iio a, g _ b.2
Derivative of a family of normal ordinal functions
Informal description
The derivative of a family of normal ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ at an ordinal $o$ is defined by transfinite recursion: - For $o = 0$, it is the next common fixed point of $f$ above $0$ - For a successor ordinal $o = \text{succ}\, o'$, it is the next common fixed point of $f$ above $\text{succ}(\text{derivFamily}\, f\, o')$ - For a limit ordinal $o$, it is the supremum of $\text{derivFamily}\, f\, b$ for all $b < o$ This sequence enumerates the common fixed points of the family $f$.
Ordinal.derivFamily_zero theorem
(f : ι → Ordinal → Ordinal) : derivFamily f 0 = nfpFamily f 0
Full source 
@[simp]
theorem derivFamily_zero (f : ι → Ordinal → Ordinal) :
    derivFamily f 0 = nfpFamily f 0 :=
  limitRecOn_zero ..
Derivative at Zero Equals Next Fixed Point
Informal description
For any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$, the derivative of $f$ at zero equals the next common fixed point of $f$ above zero, i.e., $$\text{derivFamily}\, f\, 0 = \text{nfpFamily}\, f\, 0.$$
Ordinal.derivFamily_succ theorem
(f : ι → Ordinal → Ordinal) (o) : derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o))
Full source 
@[simp]
theorem derivFamily_succ (f : ι → Ordinal → Ordinal) (o) :
    derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o)) :=
  limitRecOn_succ ..
Derivative of a Family of Ordinal Functions at Successor Ordinals
Informal description
For any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ and any ordinal $o$, the derivative of $f$ at the successor ordinal $\text{succ}\, o$ is equal to the next common fixed point of $f$ above $\text{succ}(\text{derivFamily}\, f\, o)$. That is, $$\text{derivFamily}\, f\, (\text{succ}\, o) = \text{nfpFamily}\, f\, (\text{succ}\, (\text{derivFamily}\, f\, o)).$$
Ordinal.derivFamily_limit theorem
(f : ι → Ordinal → Ordinal) {o} : IsLimit o → derivFamily f o = ⨆ b : Set.Iio o, derivFamily f b
Full source 
theorem derivFamily_limit (f : ι → Ordinal → Ordinal) {o} :
    IsLimit o → derivFamily f o = ⨆ b : Set.Iio o, derivFamily f b :=
  limitRecOn_limit _ _ _ _
Derivative of a Family of Ordinal Functions at a Limit Ordinal
Informal description
For a family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$ and a limit ordinal $o$, the derivative of $f$ at $o$ equals the supremum of the derivatives of $f$ at all ordinals less than $o$. That is, $$\text{derivFamily}\, f\, o = \bigsqcup_{b < o} \text{derivFamily}\, f\, b.$$
Ordinal.isNormal_derivFamily theorem
[Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) : IsNormal (derivFamily f)
Full source 
theorem isNormal_derivFamily [Small.{u} ι] (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) :
    IsNormal (derivFamily f) := by
  refine ⟨fun o ↦ ?_, fun o h a ↦ ?_⟩
  · rw [derivFamily_succ, ← succ_le_iff]
    exact le_nfpFamily _ _
  · simp_rw [derivFamily_limit _ h, Ordinal.iSup_le_iff, Subtype.forall, Set.mem_Iio]
Normality of the Derivative of a Family of Ordinal Functions
Informal description
For any $u$-small type $\iota$ and any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$, the derivative function $\text{derivFamily}\, f$ is normal. That is, it is strictly increasing and continuous (preserves suprema of increasing sequences).
Ordinal.derivFamily_strictMono theorem
[Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) : StrictMono (derivFamily f)
Full source 
theorem derivFamily_strictMono [Small.{u} ι] (f : ι → OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) :
    StrictMono (derivFamily f) :=
  (isNormal_derivFamily f).strictMono
Strict Monotonicity of the Derivative of a Family of Ordinal Functions
Informal description
For any $u$-small type $\iota$ and any family of ordinal functions $f : \iota \to \text{Ordinal} \to \text{Ordinal}$, the derivative function $\text{derivFamily}\, f$ is strictly increasing. That is, for any ordinals $a < b$, we have $\text{derivFamily}\, f\, a < \text{derivFamily}\, f\, b$.
Ordinal.derivFamily_fp theorem
[Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) : f i (derivFamily f o) = derivFamily f o
Full source 
theorem derivFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) :
    f i (derivFamily f o) = derivFamily f o := by
  induction' o using limitRecOn with o _ o l IH
  · rw [derivFamily_zero]
    exact nfpFamily_fp H 0
  · rw [derivFamily_succ]
    exact nfpFamily_fp H _
  · have : Nonempty (Set.Iio o) := ⟨0, l.pos⟩
    rw [derivFamily_limit _ l, H.map_iSup]
    refine eq_of_forall_ge_iff fun c => ?_
    rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]
    refine forall_congr' fun a ↦ ?_
    rw [IH _ a.2]
Fixed Point Property of Derivative for Normal Ordinal Functions
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a $u$-small type $\iota$. For any $i \in \iota$ and any ordinal $o$, the function $f_i$ evaluated at the derivative $\text{derivFamily}\, f\, o$ equals $\text{derivFamily}\, f\, o$, i.e., $f_i(\text{derivFamily}\, f\, o) = \text{derivFamily}\, f\, o$.
Ordinal.le_iff_derivFamily theorem
[Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} : (∀ i, f i a ≤ a) ↔ ∃ o, derivFamily f o = a
Full source 
theorem le_iff_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} :
    (∀ i, f i a ≤ a) ↔ ∃ o, derivFamily f o = a :=
  ⟨fun ha => by
    suffices ∀ (o), a ≤ derivFamily f o → ∃ o, derivFamily f o = a from
      this a (isNormal_derivFamily _).le_apply
    intro o
    induction' o using limitRecOn with o IH o l IH
    · intro h₁
      refine ⟨0, le_antisymm ?_ h₁⟩
      rw [derivFamily_zero]
      exact nfpFamily_le_fp (fun i => (H i).monotone) (Ordinal.zero_le _) ha
    · intro h₁
      rcases le_or_lt a (derivFamily f o) with h | h
      · exact IH h
      refine ⟨succ o, le_antisymm ?_ h₁⟩
      rw [derivFamily_succ]
      exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
    · intro h₁
      rcases eq_or_lt_of_le h₁ with h | h
      · exact ⟨_, h.symm⟩
      rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h
      obtain ⟨o', h⟩ := h
      exact IH o' o'.2 (le_of_not_le h),
    fun ⟨_, e⟩ i => e ▸ (derivFamily_fp (H i) _).le⟩
Characterization of Ordinals Above Fixed Points via Derivatives
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a $u$-small type $\iota$. For any ordinal $a$, the following are equivalent: 1. For every $i \in \iota$, $f_i(a) \leq a$. 2. There exists an ordinal $o$ such that $\text{derivFamily}\, f\, o = a$.
Ordinal.fp_iff_derivFamily theorem
[Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} : (∀ i, f i a = a) ↔ ∃ o, derivFamily f o = a
Full source 
theorem fp_iff_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} :
    (∀ i, f i a = a) ↔ ∃ o, derivFamily f o = a :=
  Iff.trans ⟨fun h i => le_of_eq (h i), fun h i => (H i).le_iff_eq.1 (h i)⟩ (le_iff_derivFamily H)
Characterization of Fixed Points via Derivatives of Normal Function Families
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a small type $\iota$. For any ordinal $a$, the following are equivalent: 1. For every $i \in \iota$, $a$ is a fixed point of $f_i$ (i.e., $f_i(a) = a$). 2. There exists an ordinal $o$ such that the $o$-th derivative of the family $f$ equals $a$ (i.e., $\text{derivFamily}\, f\, o = a$).
Ordinal.derivFamily_eq_enumOrd theorem
[Small.{u} ι] (H : ∀ i, IsNormal (f i)) : derivFamily f = enumOrd (⋂ i, Function.fixedPoints (f i))
Full source 
/-- For a family of normal functions, `Ordinal.derivFamily` enumerates the common fixed points. -/
theorem derivFamily_eq_enumOrd [Small.{u} ι] (H : ∀ i, IsNormal (f i)) :
    derivFamily f = enumOrd (⋂ i, Function.fixedPoints (f i)) := by
  rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]
  use (isNormal_derivFamily f).strictMono
  rw [Set.range_eq_iff]
  refine ⟨?_, fun a ha => ?_⟩
  · rintro a S ⟨i, hi⟩
    rw [← hi]
    exact derivFamily_fp (H i) a
  rw [Set.mem_iInter] at ha
  rwa [← fp_iff_derivFamily H]
Derivative of Normal Function Family Enumerates Common Fixed Points
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of normal ordinal functions indexed by a small type $\iota$. Then the derivative function $\text{derivFamily}\, f$ enumerates the common fixed points of the family $f_i$, i.e., it equals the enumeration function of the intersection $\bigcap_i \{x \mid f_i(x) = x\}$.
Ordinal.nfp definition
(f : Ordinal → Ordinal) : Ordinal → Ordinal
Full source 
/-- The next fixed point function, the least fixed point of the normal function `f`, at least `a`.

This is defined as `nfpFamily` applied to a family consisting only of `f`. -/
def nfp (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
  nfpFamily fun _ : Unit => f
Next fixed point of a normal ordinal function
Informal description
The next fixed point function, denoted $\text{nfp}\, f\, a$, is the least fixed point of the normal function $f$ that is at least $a$. It is defined as the supremum of all ordinals obtained by iterating $f$ starting from $a$, i.e., $\text{nfp}\, f\, a = \bigsqcup_{n \in \mathbb{N}} f^n(a)$.
Ordinal.nfp_eq_nfpFamily theorem
(f : Ordinal → Ordinal) : nfp f = nfpFamily fun _ : Unit => f
Full source 
theorem nfp_eq_nfpFamily (f : Ordinal → Ordinal) : nfp f = nfpFamily fun _ : Unit => f :=
  rfl
Equality of next fixed point functions: $\text{nfp}\, f = \text{nfpFamily}\, (\lambda \_, f)$
Informal description
For any normal ordinal function $f$, the next fixed point function $\text{nfp}\, f$ is equal to the next common fixed point function $\text{nfpFamily}$ applied to the constant family $\lambda \_ : \text{Unit}, f$.
Ordinal.iSup_iterate_eq_nfp theorem
(f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) : ⨆ n : ℕ, f^[n] a = nfp f a
Full source 
theorem iSup_iterate_eq_nfp (f : OrdinalOrdinal.{u} → OrdinalOrdinal.{u}) (a : OrdinalOrdinal.{u}) :
    ⨆ n : ℕ, f^[n] a = nfp f a := by
  apply le_antisymm
  · rw [Ordinal.iSup_le_iff]
    intro n
    rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]
    exact Ordinal.le_iSup _ _
  · apply Ordinal.iSup_le
    intro l
    rw [List.foldr_const f a l]
    exact Ordinal.le_iSup _ _
Supremum of Iterates Equals Next Fixed Point
Informal description
For any normal function $f$ on ordinals and any ordinal $a$, the supremum of the iterates $f^n(a)$ over all natural numbers $n$ is equal to the next fixed point $\mathrm{nfp}\,f\,a$ of $f$ above $a$. That is, \[ \bigsqcup_{n \in \mathbb{N}} f^n(a) = \mathrm{nfp}\,f\,a. \]
Ordinal.iterate_le_nfp theorem
(f a n) : f^[n] a ≤ nfp f a
Full source 
theorem iterate_le_nfp (f a n) : f^[n] a ≤ nfp f a := by
  rw [← iSup_iterate_eq_nfp]
  exact Ordinal.le_iSup (fun n ↦ f^[n] a) n
Iterates Bounded by Next Fixed Point: $f^n(a) \leq \mathrm{nfp}\,f\,a$
Informal description
For any normal ordinal function $f$, any ordinal $a$, and any natural number $n$, the $n$-th iterate $f^n(a)$ is less than or equal to the next fixed point $\mathrm{nfp}\,f\,a$ of $f$ above $a$. That is, \[ f^n(a) \leq \mathrm{nfp}\,f\,a. \]
Ordinal.le_nfp theorem
(f a) : a ≤ nfp f a
Full source 
theorem le_nfp (f a) : a ≤ nfp f a :=
  iterate_le_nfp f a 0
Initial Ordinal Below Next Fixed Point: $a \leq \mathrm{nfp}\,f\,a$
Informal description
For any normal ordinal function $f$ and any ordinal $a$, the ordinal $a$ is less than or equal to the next fixed point $\mathrm{nfp}\,f\,a$ of $f$ above $a$. That is, \[ a \leq \mathrm{nfp}\,f\,a. \]
Ordinal.lt_nfp_iff theorem
{a b} : a < nfp f b ↔ ∃ n, a < f^[n] b
Full source 
theorem lt_nfp_iff {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := by
  rw [← iSup_iterate_eq_nfp]
  exact Ordinal.lt_iSup_iff
Characterization of ordinals below the next fixed point via iterates
Informal description
For any normal function $f$ on ordinals and ordinals $a$ and $b$, we have $a < \mathrm{nfp}\,f\,b$ if and only if there exists a natural number $n$ such that $a < f^n(b)$, where $f^n$ denotes the $n$-th iterate of $f$.
Ordinal.nfp_le_iff theorem
{a b} : nfp f a ≤ b ↔ ∀ n, f^[n] a ≤ b
Full source 
theorem nfp_le_iff {a b} : nfpnfp f a ≤ b ↔ ∀ n, f^[n] a ≤ b := by
  rw [← iSup_iterate_eq_nfp]
  exact Ordinal.iSup_le_iff
Characterization of Next Fixed Point: $\mathrm{nfp}\,f\,a \leq b \leftrightarrow \forall n,\, f^n(a) \leq b$
Informal description
For any normal function $f$ on ordinals and ordinals $a, b$, the next fixed point $\mathrm{nfp}\,f\,a$ is less than or equal to $b$ if and only if for every natural number $n$, the $n$-th iterate $f^n(a)$ is less than or equal to $b$. That is, \[ \mathrm{nfp}\,f\,a \leq b \leftrightarrow \forall n \in \mathbb{N},\, f^n(a) \leq b. \]
Ordinal.nfp_le theorem
{a b} : (∀ n, f^[n] a ≤ b) → nfp f a ≤ b
Full source 
theorem nfp_le {a b} : (∀ n, f^[n] a ≤ b) → nfp f a ≤ b :=
  nfp_le_iff.2
Upper Bound Characterization of Next Fixed Point: $\forall n, f^n(a) \leq b \Rightarrow \mathrm{nfp}\,f\,a \leq b$
Informal description
For any normal function $f$ on ordinals and ordinals $a, b$, if for every natural number $n$ the $n$-th iterate $f^n(a)$ is less than or equal to $b$, then the next fixed point $\mathrm{nfp}\,f\,a$ is less than or equal to $b$.
Ordinal.nfp_id theorem
: nfp id = id
Full source 
@[simp]
theorem nfp_id : nfp id = id := by
  ext
  simp_rw [← iSup_iterate_eq_nfp, iterate_id]
  exact ciSup_const
Next Fixed Point of Identity Function: $\text{nfp}(\mathrm{id}) = \mathrm{id}$
Informal description
The next fixed point of the identity function on ordinals is the identity function itself, i.e., $\text{nfp}(\mathrm{id}) = \mathrm{id}$.
Ordinal.nfp_monotone theorem
(hf : Monotone f) : Monotone (nfp f)
Full source 
theorem nfp_monotone (hf : Monotone f) : Monotone (nfp f) :=
  nfpFamily_monotone fun _ => hf
Monotonicity of the Next Fixed Point Function
Informal description
For any monotone function $f$ on ordinals, the next fixed point function $\text{nfp}\, f$ is also monotone. That is, for any ordinals $a \leq b$, we have $\text{nfp}\, f\, a \leq \text{nfp}\, f\, b$.
Ordinal.IsNormal.apply_lt_nfp theorem
(H : IsNormal f) {a b} : f b < nfp f a ↔ b < nfp f a
Full source 
theorem IsNormal.apply_lt_nfp (H : IsNormal f) {a b} : f b < nfp f a ↔ b < nfp f a := by
  unfold nfp
  rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩
Characterization of ordinals below the next fixed point of a normal function: $f(b) < \text{nfp}\,f\,a$ ↔ $b < \text{nfp}\,f\,a$
Informal description
Let $f$ be a normal ordinal function. For any ordinals $a$ and $b$, we have $f(b) < \text{nfp}\,f\,a$ if and only if $b < \text{nfp}\,f\,a$, where $\text{nfp}\,f\,a$ is the next fixed point of $f$ above $a$.
Ordinal.IsNormal.nfp_le_apply theorem
(H : IsNormal f) {a b} : nfp f a ≤ f b ↔ nfp f a ≤ b
Full source 
theorem IsNormal.nfp_le_apply (H : IsNormal f) {a b} : nfpnfp f a ≤ f b ↔ nfp f a ≤ b :=
  le_iff_le_iff_lt_iff_lt.2 H.apply_lt_nfp
Characterization of ordinals above the next fixed point of a normal function: $\text{nfp}\,f\,a \leq f(b) \leftrightarrow \text{nfp}\,f\,a \leq b$
Informal description
Let $f$ be a normal ordinal function. For any ordinals $a$ and $b$, the next fixed point $\text{nfp}\,f\,a$ satisfies $\text{nfp}\,f\,a \leq f(b)$ if and only if $\text{nfp}\,f\,a \leq b$.
Ordinal.nfp_le_fp theorem
(H : Monotone f) {a b} (ab : a ≤ b) (h : f b ≤ b) : nfp f a ≤ b
Full source 
theorem nfp_le_fp (H : Monotone f) {a b} (ab : a ≤ b) (h : f b ≤ b) : nfp f a ≤ b :=
  nfpFamily_le_fp (fun _ => H) ab fun _ => h
Next Fixed Point is Least Upper Bound for Monotone Functions
Informal description
Let $f$ be a monotone function on ordinals, and let $a, b$ be ordinals such that $a \leq b$ and $f(b) \leq b$. Then the next fixed point of $f$ above $a$ satisfies $\text{nfp}\, f\, a \leq b$.
Ordinal.IsNormal.nfp_fp theorem
(H : IsNormal f) : ∀ a, f (nfp f a) = nfp f a
Full source 
theorem IsNormal.nfp_fp (H : IsNormal f) : ∀ a, f (nfp f a) = nfp f a :=
  @nfpFamily_fp Unit (fun _ => f) _ () H
Fixed Point Property of Next Fixed Point for Normal Ordinal Functions
Informal description
For any normal ordinal function $f$ and any ordinal $a$, the function $f$ evaluated at the next fixed point $\text{nfp}\, f\, a$ equals $\text{nfp}\, f\, a$, i.e., $f(\text{nfp}\, f\, a) = \text{nfp}\, f\, a$.
Ordinal.IsNormal.apply_le_nfp theorem
(H : IsNormal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a
Full source 
theorem IsNormal.apply_le_nfp (H : IsNormal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
  ⟨H.le_apply.trans, fun h => by simpa only [H.nfp_fp] using H.le_iff.2 h⟩
Characterization of Next Fixed Point for Normal Ordinal Functions: $f(b) \leq \text{nfp}\, f\, a \leftrightarrow b \leq \text{nfp}\, f\, a$
Informal description
For any normal ordinal function $f$ and ordinals $a, b$, we have $f(b) \leq \text{nfp}\, f\, a$ if and only if $b \leq \text{nfp}\, f\, a$, where $\text{nfp}\, f\, a$ is the next fixed point of $f$ above $a$.
Ordinal.nfp_eq_self theorem
{a} (h : f a = a) : nfp f a = a
Full source 
theorem nfp_eq_self {a} (h : f a = a) : nfp f a = a :=
  nfpFamily_eq_self fun _ => h
Fixed Point Property of Next Fixed Point: $\text{nfp}\,f\,a = a$ when $f(a) = a$
Informal description
For any ordinal $a$ and any function $f$ on ordinals, if $a$ is a fixed point of $f$ (i.e., $f(a) = a$), then the next fixed point of $f$ above $a$ is equal to $a$ itself (i.e., $\text{nfp}\,f\,a = a$).
Ordinal.not_bddAbove_fp theorem
(H : IsNormal f) : ¬BddAbove (Function.fixedPoints f)
Full source 
/-- The fixed point lemma for normal functions: any normal function has an unbounded set of
fixed points. -/
theorem not_bddAbove_fp (H : IsNormal f) : ¬ BddAbove (Function.fixedPoints f) := by
  convert not_bddAbove_fp_family fun _ : Unit => H
  exact (Set.iInter_const _).symm
Unboundedness of Fixed Points for Normal Ordinal Functions
Informal description
For any normal ordinal function $f$, the set of fixed points $\{x \mid f(x) = x\}$ is unbounded in the ordinals. That is, for any ordinal $\alpha$, there exists a fixed point $\beta \geq \alpha$ such that $f(\beta) = \beta$.
Ordinal.deriv definition
(f : Ordinal → Ordinal) : Ordinal → Ordinal
Full source 
/-- The derivative of a normal function `f` is the sequence of fixed points of `f`.

This is defined as `Ordinal.derivFamily` applied to a trivial family consisting only of `f`. -/
def deriv (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
  derivFamily fun _ : Unit => f
Derivative of a normal ordinal function
Informal description
The derivative of a normal ordinal function $f$ is the sequence of fixed points of $f$, defined as $\text{derivFamily}$ applied to the trivial family consisting only of $f$. For an ordinal $o$, the derivative is computed by transfinite recursion: - $\text{deriv}\, f\, 0$ is the next fixed point of $f$ above $0$ - For successor ordinals, $\text{deriv}\, f\, (\text{succ}\, o')$ is the next fixed point of $f$ above $\text{succ}(\text{deriv}\, f\, o')$ - For limit ordinals $o$, $\text{deriv}\, f\, o$ is the supremum of $\text{deriv}\, f\, b$ for all $b < o$ This sequence enumerates all fixed points of the normal function $f$.
Ordinal.deriv_eq_derivFamily theorem
(f : Ordinal → Ordinal) : deriv f = derivFamily fun _ : Unit => f
Full source 
theorem deriv_eq_derivFamily (f : Ordinal → Ordinal) : deriv f = derivFamily fun _ : Unit => f :=
  rfl
Derivative Equals Derivative of Trivial Family
Informal description
For any normal ordinal function $f$, the derivative function $\text{deriv}\, f$ is equal to the derivative of the trivial family consisting only of $f$, i.e., $\text{derivFamily}\, (\lambda \_ : \text{Unit}, f)$.
Ordinal.deriv_zero_right theorem
(f) : deriv f 0 = nfp f 0
Full source 
@[simp]
theorem deriv_zero_right (f) : deriv f 0 = nfp f 0 :=
  derivFamily_zero _
Derivative at Zero Equals Next Fixed Point
Informal description
For any normal ordinal function $f$, the derivative of $f$ at zero equals the next fixed point of $f$ above zero, i.e., $$\text{deriv}\, f\, 0 = \text{nfp}\, f\, 0.$$
Ordinal.deriv_succ theorem
(f o) : deriv f (succ o) = nfp f (succ (deriv f o))
Full source 
@[simp]
theorem deriv_succ (f o) : deriv f (succ o) = nfp f (succ (deriv f o)) :=
  derivFamily_succ _ _
Derivative of Normal Function at Successor Ordinals
Informal description
For any normal ordinal function $f$ and any ordinal $o$, the derivative of $f$ at the successor ordinal $\text{succ}\, o$ equals the next fixed point of $f$ above $\text{succ}(\text{deriv}\, f\, o)$. That is, $$\text{deriv}\, f\, (\text{succ}\, o) = \text{nfp}\, f\, (\text{succ}\, (\text{deriv}\, f\, o)).$$
Ordinal.deriv_limit theorem
(f) {o} : IsLimit o → deriv f o = ⨆ a : { a // a < o }, deriv f a
Full source 
theorem deriv_limit (f) {o} : IsLimit o → deriv f o = ⨆ a : {a // a < o}, deriv f a :=
  derivFamily_limit _
Derivative of Normal Function at Limit Ordinals Equals Supremum of Preceding Derivatives
Informal description
For any normal ordinal function $f$ and any limit ordinal $o$, the derivative of $f$ at $o$ equals the supremum of the derivatives of $f$ at all ordinals less than $o$. That is, $$\text{deriv}\, f\, o = \bigsqcup_{a < o} \text{deriv}\, f\, a.$$
Ordinal.isNormal_deriv theorem
(f) : IsNormal (deriv f)
Full source 
theorem isNormal_deriv (f) : IsNormal (deriv f) :=
  isNormal_derivFamily _
Normality of the Derivative of a Normal Ordinal Function
Informal description
For any normal ordinal function $f$, the derivative function $\mathrm{deriv}\, f$ is normal. That is: 1. It is strictly increasing: for any ordinals $a < b$, we have $\mathrm{deriv}\, f\, a < \mathrm{deriv}\, f\, b$. 2. It is continuous: for any limit ordinal $o$, we have $\mathrm{deriv}\, f\, o = \sup_{a < o} \mathrm{deriv}\, f\, a$.
Ordinal.deriv_strictMono theorem
(f) : StrictMono (deriv f)
Full source 
theorem deriv_strictMono (f) : StrictMono (deriv f) :=
  derivFamily_strictMono _
Strict Monotonicity of the Derivative of a Normal Ordinal Function
Informal description
For any normal ordinal function $f$, the derivative function $\mathrm{deriv}\, f$ is strictly increasing. That is, for any ordinals $a < b$, we have $\mathrm{deriv}\, f\, a < \mathrm{deriv}\, f\, b$.
Ordinal.deriv_id_of_nfp_id theorem
(h : nfp f = id) : deriv f = id
Full source 
theorem deriv_id_of_nfp_id (h : nfp f = id) : deriv f = id :=
  ((isNormal_deriv _).eq_iff_zero_and_succ IsNormal.refl).2 (by simp [h])
Derivative Equals Identity When Next Fixed Point is Identity
Informal description
If the next fixed point function $\text{nfp}\, f$ of a normal ordinal function $f$ is equal to the identity function, then the derivative of $f$ is also equal to the identity function. That is, if $\text{nfp}\, f = \text{id}$, then $\text{deriv}\, f = \text{id}$.
Ordinal.IsNormal.deriv_fp theorem
(H : IsNormal f) : ∀ o, f (deriv f o) = deriv f o
Full source 
theorem IsNormal.deriv_fp (H : IsNormal f) : ∀ o, f (deriv f o) = deriv f o :=
  derivFamily_fp (i := ⟨⟩) H
Fixed Point Property of the Derivative for Normal Ordinal Functions
Informal description
For any normal ordinal function $f$ and any ordinal $o$, the derivative of $f$ at $o$ is a fixed point of $f$, i.e., $f(\text{deriv}\, f\, o) = \text{deriv}\, f\, o$.
Ordinal.IsNormal.le_iff_deriv theorem
(H : IsNormal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a
Full source 
theorem IsNormal.le_iff_deriv (H : IsNormal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a := by
  unfold deriv
  rw [← le_iff_derivFamily fun _ : Unit => H]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩
Characterization of Ordinals Above Fixed Points via Derivatives for Normal Functions
Informal description
For a normal ordinal function $f$ and any ordinal $a$, the following are equivalent: 1. $f(a) \leq a$; 2. There exists an ordinal $o$ such that the derivative of $f$ at $o$ equals $a$, i.e., $\text{deriv}\, f\, o = a$.
Ordinal.IsNormal.fp_iff_deriv theorem
(H : IsNormal f) {a} : f a = a ↔ ∃ o, deriv f o = a
Full source 
theorem IsNormal.fp_iff_deriv (H : IsNormal f) {a} : f a = a ↔ ∃ o, deriv f o = a := by
  rw [← H.le_iff_eq, H.le_iff_deriv]
Fixed Point Characterization via Derivatives for Normal Ordinal Functions
Informal description
For a normal ordinal function $f$ and any ordinal $a$, the following are equivalent: 1. $a$ is a fixed point of $f$, i.e., $f(a) = a$; 2. There exists an ordinal $o$ such that the derivative of $f$ at $o$ equals $a$, i.e., $\mathrm{deriv}\,f\,o = a$.
Ordinal.deriv_eq_enumOrd theorem
(H : IsNormal f) : deriv f = enumOrd (Function.fixedPoints f)
Full source 
/-- `Ordinal.deriv` enumerates the fixed points of a normal function. -/
theorem deriv_eq_enumOrd (H : IsNormal f) : deriv f = enumOrd (Function.fixedPoints f) := by
  convert derivFamily_eq_enumOrd fun _ : Unit => H
  exact (Set.iInter_const _).symm
Derivative of Normal Function Enumerates Fixed Points
Informal description
For any normal ordinal function $f$, the derivative function $\mathrm{deriv}\,f$ enumerates the fixed points of $f$, i.e., it equals the enumeration function of the set $\{x \mid f(x) = x\}$.
Ordinal.deriv_eq_id_of_nfp_eq_id theorem
(h : nfp f = id) : deriv f = id
Full source 
theorem deriv_eq_id_of_nfp_eq_id (h : nfp f = id) : deriv f = id :=
  (IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) IsNormal.refl).2 <| by simp [h]
Derivative is Identity when Next Fixed Point is Identity
Informal description
If the next fixed point function $\mathrm{nfp}\,f$ of a normal ordinal function $f$ is the identity function, then the derivative function $\mathrm{deriv}\,f$ is also the identity function. That is, if $\mathrm{nfp}\,f = \mathrm{id}$, then $\mathrm{deriv}\,f = \mathrm{id}$.
Ordinal.nfp_zero theorem
: nfp 0 = id
Full source 
@[simp]
theorem nfp_zero : nfp 0 = id := by
  ext
  exact nfp_zero_left _
Next Fixed Point of Zero Function is Identity
Informal description
The next fixed point function of the zero function is the identity function on ordinals, i.e., $\mathrm{nfp}\,0 = \mathrm{id}$.
Ordinal.deriv_zero theorem
: deriv 0 = id
Full source 
@[simp]
theorem deriv_zero : deriv 0 = id :=
  deriv_eq_id_of_nfp_eq_id nfp_zero
Derivative of Zero Function is Identity
Informal description
The derivative of the zero function on ordinals is the identity function, i.e., $\mathrm{deriv}\,0 = \mathrm{id}$.
Ordinal.deriv_zero_left theorem
(a) : deriv 0 a = a
Full source 
theorem deriv_zero_left (a) : deriv 0 a = a := by
  rw [deriv_zero, id_eq]
Derivative of Zero Function at Any Ordinal is Identity
Informal description
For any ordinal $a$, the derivative of the zero function evaluated at $a$ is equal to $a$, i.e., $\mathrm{deriv}\,0\,a = a$.
Ordinal.nfp_add_zero theorem
(a) : nfp (a + ·) 0 = a * ω
Full source 
@[simp]
theorem nfp_add_zero (a) : nfp (a + ·) 0 = a * ω := by
  simp_rw [← iSup_iterate_eq_nfp, ← iSup_mul_nat]
  congr; funext n
  induction' n with n hn
  · rw [Nat.cast_zero, mul_zero, iterate_zero_apply]
  · rw [iterate_succ_apply', Nat.add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, hn]
Next Fixed Point of Addition from Zero: $\text{nfp}\, (\lambda b, a + b)\, 0 = a \cdot \omega$
Informal description
For any ordinal $a$, the next fixed point of the function $\lambda b, a + b$ starting from $0$ is equal to $a \cdot \omega$, i.e., $\text{nfp}\, (\lambda b, a + b)\, 0 = a \cdot \omega$.
Ordinal.nfp_add_eq_mul_omega0 theorem
{a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * ω
Full source 
theorem nfp_add_eq_mul_omega0 {a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * ω := by
  apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
  · rw [← nfp_add_zero]
    exact nfp_monotone (isNormal_add_right a).monotone (Ordinal.zero_le b)
  · dsimp; rw [← mul_one_add, one_add_omega0]
Next Fixed Point of Addition: $\text{nfp}\, (\lambda x, a + x)\, b = a \cdot \omega$ when $b \leq a \cdot \omega$
Informal description
For any ordinals $a$ and $b$ such that $b \leq a \cdot \omega$, the next fixed point of the function $\lambda x, a + x$ starting from $b$ is equal to $a \cdot \omega$, i.e., $\text{nfp}\, (\lambda x, a + x)\, b = a \cdot \omega$.
Ordinal.add_eq_right_iff_mul_omega0_le theorem
{a b : Ordinal} : a + b = b ↔ a * ω ≤ b
Full source 
theorem add_eq_right_iff_mul_omega0_le {a b : Ordinal} : a + b = b ↔ a * ω ≤ b := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← nfp_add_zero a, ← deriv_zero_right]
    obtain ⟨c, hc⟩ := (isNormal_add_right a).fp_iff_deriv.1 h
    rw [← hc]
    exact (isNormal_deriv _).monotone (Ordinal.zero_le _)
  · have := Ordinal.add_sub_cancel_of_le h
    nth_rw 1 [← this]
    rwa [← add_assoc, ← mul_one_add, one_add_omega0]
Fixed Point Criterion for Ordinal Addition: $a + b = b \leftrightarrow a \cdot \omega \leq b$
Informal description
For any ordinals $a$ and $b$, the equality $a + b = b$ holds if and only if $a \cdot \omega \leq b$.
Ordinal.add_le_right_iff_mul_omega0_le theorem
{a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b
Full source 
theorem add_le_right_iff_mul_omega0_le {a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b := by
  rw [← add_eq_right_iff_mul_omega0_le]
  exact (isNormal_add_right a).le_iff_eq
Fixed Point Inequality Criterion for Ordinal Addition: $a + b \leq b \leftrightarrow a \cdot \omega \leq b$
Informal description
For any ordinals $a$ and $b$, the inequality $a + b \leq b$ holds if and only if $a \cdot \omega \leq b$.
Ordinal.deriv_add_eq_mul_omega0_add theorem
(a b : Ordinal.{u}) : deriv (a + ·) b = a * ω + b
Full source 
theorem deriv_add_eq_mul_omega0_add (a b : OrdinalOrdinal.{u}) : deriv (a + ·) b = a * ω + b := by
  revert b
  rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_add_right _)]
  refine ⟨?_, fun a h => ?_⟩
  · rw [deriv_zero_right, add_zero]
    exact nfp_add_zero a
  · rw [deriv_succ, h, add_succ]
    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 ((le_add_right _ _).trans (le_succ _)))
Derivative of Addition Function: $\mathrm{deriv}\,(\lambda x, a + x)\,b = a \cdot \omega + b$
Informal description
For any ordinals $a$ and $b$, the derivative of the function $\lambda x, a + x$ at $b$ equals $a \cdot \omega + b$. That is, $$\mathrm{deriv}\,(\lambda x, a + x)\,b = a \cdot \omega + b.$$
Ordinal.nfp_mul_one theorem
{a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = a ^ ω
Full source 
@[simp]
theorem nfp_mul_one {a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = a ^ ω := by
  rw [← iSup_iterate_eq_nfp, ← iSup_pow ha]
  congr
  funext n
  induction' n with n hn
  · rw [pow_zero, iterate_zero_apply]
  · rw [iterate_succ_apply', Nat.add_comm, pow_add, pow_one, hn]
Next Fixed Point of Multiplication by $a$ at $1$ is $a^\omega$
Informal description
For any ordinal $a > 0$, the next fixed point of the multiplication-by-$a$ function starting from $1$ is equal to $a^\omega$, i.e., $\mathrm{nfp}\,(a \cdot \cdot)\,1 = a^\omega$.
Ordinal.nfp_mul_zero theorem
(a : Ordinal) : nfp (a * ·) 0 = 0
Full source 
@[simp]
theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0 := by
  rw [← Ordinal.le_zero, nfp_le_iff]
  intro n
  induction' n with n hn; · rfl
  dsimp only; rwa [iterate_succ_apply, mul_zero]
Next Fixed Point of Multiplication by $a$ at Zero is Zero
Informal description
For any ordinal $a$, the next fixed point of the multiplication-by-$a$ function starting from $0$ is $0$, i.e., $\mathrm{nfp}\,(a \cdot \cdot)\,0 = 0$.
Ordinal.nfp_mul_eq_opow_omega0 theorem
{a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) : nfp (a * ·) b = a ^ ω
Full source 
theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) :
    nfp (a * ·) b = a ^ ω := by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_opow omega0_ne_zero] at hba ⊢
    simp_rw [Ordinal.le_zero.1 hba, zero_mul]
    exact nfp_zero_left 0
  apply le_antisymm
  · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]
  rw [← nfp_mul_one ha]
  exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)
Next Fixed Point of Multiplication by $a$ Starting from $b$ is $a^\omega$ for $0 < b \leq a^\omega$
Informal description
For any ordinals $a$ and $b$ with $0 < b$ and $b \leq a^\omega$, the next fixed point of the multiplication-by-$a$ function starting from $b$ is equal to $a^\omega$, i.e., $\mathrm{nfp}\,(a \cdot \cdot)\,b = a^\omega$.
Ordinal.mul_eq_right_iff_opow_omega0_dvd theorem
{a b : Ordinal} : a * b = b ↔ a ^ ω ∣ b
Full source 
theorem mul_eq_right_iff_opow_omega0_dvd {a b : Ordinal} : a * b = b ↔ a ^ ω ∣ b := by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]
    exact eq_comm
  refine ⟨fun hab => ?_, fun h => ?_⟩
  · rw [dvd_iff_mod_eq_zero]
    rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
      add_left_cancel_iff] at hab
    rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab
    · exact hab
    refine (not_lt_of_le hab (mod_lt b (opow_ne_zero ω ?_))).elim
    rwa [← Ordinal.pos_iff_ne_zero]
  obtain ⟨c, hc⟩ := h
  rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
Characterization of Multiplication Fixed Points via $\omega$-Power Divisibility
Informal description
For any ordinals $a$ and $b$, the equality $a \cdot b = b$ holds if and only if $a^\omega$ divides $b$.
Ordinal.mul_le_right_iff_opow_omega0_dvd theorem
{a b : Ordinal} (ha : 0 < a) : a * b ≤ b ↔ (a ^ ω) ∣ b
Full source 
theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) :
    a * b ≤ b ↔ (a ^ ω) ∣ b := by
  rw [← mul_eq_right_iff_opow_omega0_dvd]
  exact (isNormal_mul_right ha).le_iff_eq
Characterization of Multiplication Upper Bounds via $\omega$-Power Divisibility
Informal description
For any ordinals $a$ and $b$ with $a > 0$, the inequality $a \cdot b \leq b$ holds if and only if $a^\omega$ divides $b$.
Ordinal.nfp_mul_opow_omega0_add theorem
{a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ ω) : nfp (a * ·) (a ^ ω * b + c) = a ^ ω * succ b
Full source 
theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c)
    (hca : c ≤ a ^ ω) : nfp (a * ·) (a ^ ω * b + c) = a ^ ω * succ b := by
  apply le_antisymm
  · apply nfp_le_fp (isNormal_mul_right ha).monotone
    · rw [mul_succ]
      apply add_le_add_left hca
    · dsimp only; rw [← mul_assoc, ← opow_one_add, one_add_omega0]
  · obtain ⟨d, hd⟩ :=
      mul_eq_right_iff_opow_omega0_dvd.1 ((isNormal_mul_right ha).nfp_fp ((a ^ ω) * b + c))
    rw [hd]
    apply mul_le_mul_left'
    have := le_nfp (a * ·) (a ^ ω * b + c)
    rw [hd] at this
    have := (add_lt_add_left hc (a ^ ω * b)).trans_le this
    rw [add_zero, mul_lt_mul_iff_left (opow_pos ω ha)] at this
    rwa [succ_le_iff]
Next fixed point of multiplication by $a$ at $a^\omega \cdot b + c$ is $a^\omega \cdot (b + 1)$
Informal description
For ordinals $a, b, c$ with $0 < a$, $0 < c$, and $c \leq a^\omega$, the next fixed point of the multiplication-by-$a$ function starting from $a^\omega \cdot b + c$ is equal to $a^\omega \cdot (b + 1)$. That is, \[ \mathrm{nfp}\,(a \cdot \cdot)\,(a^\omega \cdot b + c) = a^\omega \cdot \mathrm{succ}\,b. \]
Ordinal.deriv_mul_eq_opow_omega0_mul theorem
{a : Ordinal.{u}} (ha : 0 < a) (b) : deriv (a * ·) b = a ^ ω * b
Full source 
theorem deriv_mul_eq_opow_omega0_mul {a : OrdinalOrdinal.{u}} (ha : 0 < a) (b) :
    deriv (a * ·) b = a ^ ω * b := by
  revert b
  rw [← funext_iff,
    IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))]
  refine ⟨?_, fun c h => ?_⟩
  · dsimp only; rw [deriv_zero_right, nfp_mul_zero, mul_zero]
  · rw [deriv_succ, h]
    exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))
Derivative of Multiplication-by-$a$: $\mathrm{deriv}\,(a \cdot \cdot)\,b = a^\omega \cdot b$
Informal description
For any ordinal $a > 0$ and any ordinal $b$, the derivative of the multiplication-by-$a$ function evaluated at $b$ equals $a^\omega \cdot b$, i.e., \[ \mathrm{deriv}\,(a \cdot \cdot)\,b = a^\omega \cdot b. \]