Ordinal Approximants for the Fixed points on complete lattices

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

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 approximation of the least fixed point greater or equal then an initial value of a bundled monotone function.
• OrdinalApprox.gfpApprox: The ordinal approximation of the greatest fixed point less or equal then an initial value of a bundled monotone function.

Main theorems

• OrdinalApprox.lfp_mem_range_lfpApprox: The approximation of the least fixed point eventually reaches the least fixed point
• OrdinalApprox.gfp_mem_range_gfpApprox: The 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][Echenique2005]
• [P. Cousot & R. Cousot, Constructive Versions of Tarski's Fixed Point Theorems][Cousot1979]

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 (Cardinal.mk α)).ord)

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

Ordinal approximants of the least fixed point greater then an initial value x

Equations

• OrdinalApprox.lfpApprox f x a = sSup ({x_1 : α | ∃ (b : Ordinal.{?u.6}) (_ : b < a), f (OrdinalApprox.lfpApprox f x b) = x_1} ∪ {x})

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

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

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

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

The ordinal approximants of the least fixed point are stabilizing when reaching a fixed point of f

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 ∧ OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b

There are distinct ordinals smaller than the successor of the domains cardinals with equal value

theorem OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h_init : x ≤ f x) (h_ab : a < b) (h_ac : a ≤ c) (h_fab : OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b) : OrdinalApprox.lfpApprox f x c ∈ Function.fixedPoints ⇑f

If there are distinct ordinals with equal value then every value succeding the smaller ordinal are fixed points

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

A fixed point of f is reached after the successor of the domains cardinality

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

Every value of the ordinal approximants are less or equal than every fixed point of f greater then the initial value

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

The least fixed point of f is reached after the successor of the domains cardinality

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

Some ordinal approximation of the least fixed point is the least fixed point.

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

Ordinal approximants of the greatest fixed point

Equations

• OrdinalApprox.gfpApprox f x a = sInf ({x_1 : α | ∃ (b : Ordinal.{?u.63}) (_ : b < a), f (OrdinalApprox.gfpApprox f x b) = x_1} ∪ {x})

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

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

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

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

The ordinal approximants of the least fixed point are stabilizing when reaching a fixed point of f

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 ∧ OrdinalApprox.gfpApprox f x a = OrdinalApprox.gfpApprox f x b

There are distinct ordinals smaller than the successor of the domains cardinals with equal value

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

A fixed point of f is reached after the successor of the domains cardinality

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

Every value of the ordinal approximants are greater or equal than every fixed point of f that is smaller then the initial value

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

The greatest fixed point of f is reached after the successor of the domains cardinality

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

Some ordinal approximation of the greatest fixed point is the greatest fixed point.