Documentation

Mathlib.SetTheory.Ordinal.FixedPointApproximants

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 #

Main theorems #

References #

Tags #

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

@[irreducible]
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
Instances For
    theorem OrdinalApprox.le_lfpApprox {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) {a : Ordinal.{u}} :
    theorem OrdinalApprox.lfpApprox_add_one {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (h : x f x) (a : Ordinal.{u}) :
    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) :

    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) :

    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) :

    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}) :

    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

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

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

    Ordinal approximants of the greatest fixed point

    Equations
    Instances For
      theorem OrdinalApprox.gfpApprox_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) {a : Ordinal.{u}} :
      theorem OrdinalApprox.gfpApprox_add_one {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (h : f x x) (a : Ordinal.{u}) :
      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) :

      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) :

      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}) :

      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

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