Ordinal Approximants for the Fixed points on complete lattices

This file sets up the ordinal-indexed approximation theory of fixed points of a monotone function in a complete lattice [CC79]. The proof follows loosely the one from [Ech05].

However, the proof given here is not constructive as we use the non-constructive axiomatization of ordinals from mathlib. It still allows an approximation scheme indexed over the ordinals.

Main definitions

• OrdinalApprox.lfpApprox: The ordinal-indexed approximation of the least fixed point greater or equal than an initial value of a bundled monotone function.
• OrdinalApprox.gfpApprox: The ordinal-indexed approximation of the greatest fixed point less or equal than an initial value of a bundled monotone function.

Main theorems

• OrdinalApprox.lfp_mem_range_lfpApprox: The ordinal-indexed approximation of the least fixed point eventually reaches the least fixed point
• OrdinalApprox.gfp_mem_range_gfpApprox: The ordinal-indexed approximation of the greatest fixed point eventually reaches the greatest fixed point

References

• F. Echenique, A short and constructive proof of Tarski’s fixed-point theorem
• P. Cousot & R. Cousot, Constructive Versions of Tarski's Fixed Point Theorems

Tags

fixed point, complete lattice, monotone function, ordinals, approximation

theorem Cardinal.not_injective_limitation_set {α : Type u} (g : Ordinal.{u} → α) : ¬Set.InjOn g (Set.Iio (SuccOrder.succ (mk α)).ord)

@[irreducible]

def OrdinalApprox.lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (a : Ordinal.{u}) : α

The ordinal-indexed sequence approximating the least fixed point greater than an initial value x. It is defined in such a way that we have lfpApprox 0 x = x and lfpApprox a x = ⨆ b < a, f (lfpApprox b x).

Equations

• OrdinalApprox.lfpApprox f x a = x ⊔ ⨆ (b : Ordinal.{?u.1}), ⨆ (_ : b < a), f (OrdinalApprox.lfpApprox f x b)

theorem OrdinalApprox.lfpApprox_mono_right {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : Monotone (lfpApprox f x)

@[deprecated OrdinalApprox.lfpApprox_mono_right (since := "2026-03-30")]

theorem OrdinalApprox.lfpApprox_monotone {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : Monotone (lfpApprox f x)

Alias of OrdinalApprox.lfpApprox_mono_right.

theorem OrdinalApprox.lfpApprox_zero {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : lfpApprox f x 0 = x

theorem OrdinalApprox.le_lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} : x ≤ lfpApprox f x a

theorem OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}} (h : a < b) : f (lfpApprox f x a) ≤ lfpApprox f x b

theorem OrdinalApprox.lfpApprox_add_one {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) (a : Ordinal.{u}) : lfpApprox f x (a + 1) = f (lfpApprox f x a)

theorem OrdinalApprox.lfpApprox_of_isSuccLimit {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (ha : Order.IsSuccLimit a) : lfpApprox f x a = ⨆ (b : ↑(Set.Iio a)), lfpApprox f x ↑b

theorem OrdinalApprox.lfpApprox_mono_left {α : Type u} [CompleteLattice α] : Monotone lfpApprox

theorem OrdinalApprox.lfpApprox_mono_mid {α : Type u} [CompleteLattice α] (f : α →o α) : Monotone (lfpApprox f)

theorem OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}} (hab : a ≤ b) (hf : lfpApprox f x a ∈ Function.fixedPoints ⇑f) : lfpApprox f x b = lfpApprox f x a

The approximations of the least fixed point stabilize at a fixed point of f

theorem OrdinalApprox.lfpApprox_eq_all_of_fixedPoint {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) : (∀ (o : Ordinal.{u}), lfpApprox f x o = x) ↔ f x = x

theorem OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b c : Ordinal.{u}} (hx : x ≤ f x) (hab : a < b) (hac : a ≤ c) (hf : lfpApprox f x a = lfpApprox f x b) : lfpApprox f x c ∈ Function.fixedPoints ⇑f

If the sequence of ordinal-indexed approximations takes a value twice, then it actually stabilised at that value.

theorem OrdinalApprox.lfpApprox_eq_of_fixedPoint_or_zero {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) (o : Ordinal.{u}) : lfpApprox f x o = x ↔ f x = x ∨ o = 0

theorem OrdinalApprox.exists_lfpApprox_eq_lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) : ∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

There are distinct indices smaller than the successor of the domain's cardinality yielding the same value

theorem OrdinalApprox.lfpApprox_ord_mem_fixedPoint {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) : lfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f

The approximation at the index of the successor of the domain's cardinality is a fixed point

theorem OrdinalApprox.lfpApprox_le_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x a : α} (ha : a ∈ Function.fixedPoints ⇑f) (hxa : x ≤ a) (i : Ordinal.{u}) : lfpApprox f x i ≤ a

Every value of the approximation is less or equal than every fixed point of f greater or equal than the initial value

theorem OrdinalApprox.lfpApprox_ord_eq_lfp {α : Type u} [CompleteLattice α] (f : α →o α) : lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = OrderHom.lfp f

The approximation sequence converges at the successor of the domain's cardinality to the least fixed point if starting from ⊥

theorem OrdinalApprox.lfp_mem_range_lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) : OrderHom.lfp f ∈ Set.range (lfpApprox f ⊥)

Some approximation of the least fixed point starting from ⊥ is the least fixed point.

theorem OrdinalApprox.iSup_lfpApprox_eq_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (hf : lfpApprox f x a ∈ Function.fixedPoints ⇑f) : ⨆ (i : Ordinal.{u}), lfpApprox f x i = lfpApprox f x a

If lfpApprox f x a is a fixed point, then the supremum of the whole ordinal-indexed sequence equals the value at a.

theorem OrdinalApprox.nextFixed_eq_iSup_lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) : ↑(f.nextFixed x hx) = ⨆ (a : Ordinal.{u}), lfpApprox f x a

The ordinal-indexed supremum of lfpApprox equals nextFixed: the least fixed point greater than or equal to x.

@[irreducible]

def OrdinalApprox.gfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (a : Ordinal.{u}) : α

The ordinal-indexed sequence approximating the greatest fixed point greater than an initial value x. It is defined in such a way that we have gfpApprox 0 x = x and gfpApprox a x = ⨅ b < a, f (lfpApprox b x).

Equations

• OrdinalApprox.gfpApprox f x a = x ⊓ ⨅ (b : Ordinal.{?u.1}), ⨅ (_ : b < a), f (OrdinalApprox.gfpApprox f x b)

theorem OrdinalApprox.gfpApprox_zero {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : gfpApprox f x 0 = x

theorem OrdinalApprox.gfpApprox_anti_right {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : Antitone (gfpApprox f x)

@[deprecated OrdinalApprox.gfpApprox_anti_right (since := "2026-03-30")]

theorem OrdinalApprox.gfpApprox_antitone {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : Antitone (gfpApprox f x)

Alias of OrdinalApprox.gfpApprox_anti_right.

theorem OrdinalApprox.gfpApprox_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} : gfpApprox f x a ≤ x

theorem OrdinalApprox.gfpApprox_add_one {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) (a : Ordinal.{u}) : gfpApprox f x (a + 1) = f (gfpApprox f x a)

theorem OrdinalApprox.gfpApprox_le_apply_gfpApprox_of_lt {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}} (h : a < b) : gfpApprox f x b ≤ f (gfpApprox f x a)

theorem OrdinalApprox.gfpApprox_of_isSuccLimit {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (ha : Order.IsSuccLimit a) : gfpApprox f x a = ⨅ (b : ↑(Set.Iio a)), gfpApprox f x ↑b

theorem OrdinalApprox.gfpApprox_mono_left {α : Type u} [CompleteLattice α] : Monotone gfpApprox

theorem OrdinalApprox.gfpApprox_mono_mid {α : Type u} [CompleteLattice α] (f : α →o α) : Monotone (gfpApprox f)

theorem OrdinalApprox.gfpApprox_eq_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}} (h_ab : a ≤ b) (h : gfpApprox f x a ∈ Function.fixedPoints ⇑f) : gfpApprox f x b = gfpApprox f x a

The approximations of the greatest fixed point stabilize at a fixed point of f

theorem OrdinalApprox.gfpApprox_eq_all_of_fixedPoint {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) : (∀ (o : Ordinal.{u}), gfpApprox f x o = x) ↔ f x = x

theorem OrdinalApprox.gfpApprox_mem_fixedPoints_of_eq {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a b c : Ordinal.{u}} (hx : f x ≤ x) (hab : a < b) (hac : a ≤ c) (hf : gfpApprox f x a = gfpApprox f x b) : gfpApprox f x c ∈ Function.fixedPoints ⇑f

theorem OrdinalApprox.gfpApprox_eq_of_fixedPoint_or_zero {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) (o : Ordinal.{u}) : gfpApprox f x o = x ↔ f x = x ∨ o = 0

theorem OrdinalApprox.exists_gfpApprox_eq_gfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} : ∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ gfpApprox f x a = gfpApprox f x b

There are distinct indices smaller than the successor of the domain's cardinality yielding the same value

theorem OrdinalApprox.gfpApprox_ord_mem_fixedPoint {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) : gfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f

The approximation at the index of the successor of the domain's cardinality is a fixed point

theorem OrdinalApprox.le_gfpApprox_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x a : α} (ha : a ∈ Function.fixedPoints ⇑f) (hax : a ≤ x) (i : Ordinal.{u}) : a ≤ gfpApprox f x i

Every value of the approximation is greater or equal than every fixed point of f less or equal than the initial value

theorem OrdinalApprox.gfpApprox_ord_eq_gfp {α : Type u} [CompleteLattice α] (f : α →o α) : gfpApprox f ⊤ (Order.succ (Cardinal.mk α)).ord = OrderHom.gfp f

The approximation sequence converges at the successor of the domain's cardinality to the greatest fixed point if starting from ⊥

theorem OrdinalApprox.gfp_mem_range_gfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) : OrderHom.gfp f ∈ Set.range (gfpApprox f ⊤)

Some approximation of the least fixed point starting from ⊤ is the greatest fixed point.

theorem OrdinalApprox.iInf_gfpApprox_eq_of_mem_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (hf : gfpApprox f x a ∈ Function.fixedPoints ⇑f) : ⨅ (i : Ordinal.{u}), gfpApprox f x i = gfpApprox f x a

If gfpApprox f x a is a fixed point, then the infimum of the whole ordinal-indexed sequence equals the value at a.

theorem OrdinalApprox.prevFixed_eq_iInf_gfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) : ↑(f.prevFixed x hx) = ⨅ (a : Ordinal.{u}), gfpApprox f x a

The ordinal-indexed infimum of gfpApprox equals prevFixed: the greatest fixed point less than or equal to x.