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 [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-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][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)

@[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 = 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_mono_left {α : Type u} [CompleteLattice α] : Monotone OrdinalApprox.lfpApprox

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

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 approximations of the least fixed point stabilize at 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 indices smaller than the successor of the domain's cardinality yielding the same 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 the sequence of ordinal-indexed approximations takes a value twice, then it actually stabilised at that value.

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

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 : α} (h_a : a ∈ Function.fixedPoints ⇑f) (h_le_init : x ≤ a) (i : Ordinal.{u}) : OrdinalApprox.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 α) : OrdinalApprox.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 (OrdinalApprox.lfpApprox f ⊥)

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

@[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 = 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_mono_left {α : Type u} [CompleteLattice α] : Monotone OrdinalApprox.gfpApprox

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

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 approximations of the greatest fixed point stabilize at 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 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 : α) (h_init : f x ≤ x) : OrdinalApprox.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 : α} (h_a : a ∈ Function.fixedPoints ⇑f) (h_le_init : a ≤ x) (i : Ordinal.{u}) : a ≤ OrdinalApprox.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 α) : OrdinalApprox.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 (OrdinalApprox.gfpApprox f ⊤)

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