Documentation

Mathlib.Order.FixedPoints

Fixed point construction on complete lattices #

This file sets up the basic theory of fixed points of a monotone function in a complete lattice.

Main definitions #

Tags #

fixed point, complete lattice, monotone function

def OrderHom.lfp {α : Type u} [CompleteLattice α] :
(α →o α) →o α

Least fixed point of a monotone function

Equations
  • OrderHom.lfp = { toFun := fun (f : α →o α) => sInf {a : α | f a a}, monotone' := }
Instances For
    def OrderHom.gfp {α : Type u} [CompleteLattice α] :
    (α →o α) →o α

    Greatest fixed point of a monotone function

    Equations
    • OrderHom.gfp = { toFun := fun (f : α →o α) => sSup {a : α | a f a}, monotone' := }
    Instances For
      theorem OrderHom.lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : f a a) :
      OrderHom.lfp f a
      theorem OrderHom.lfp_le_fixed {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : f a = a) :
      OrderHom.lfp f a
      theorem OrderHom.le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), f b ba b) :
      a OrderHom.lfp f
      theorem OrderHom.map_le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a OrderHom.lfp f) :
      f a OrderHom.lfp f
      @[simp]
      theorem OrderHom.map_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      f (OrderHom.lfp f) = OrderHom.lfp f
      theorem OrderHom.isFixedPt_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      Function.IsFixedPt (⇑f) (OrderHom.lfp f)
      theorem OrderHom.lfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : OrderHom.lfp f a) :
      OrderHom.lfp f f a
      theorem OrderHom.isLeast_lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :
      IsLeast {a : α | f a a} (OrderHom.lfp f)
      theorem OrderHom.isLeast_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      IsLeast (Function.fixedPoints f) (OrderHom.lfp f)
      theorem OrderHom.lfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : αProp} (step : ∀ (a : α), p aa OrderHom.lfp fp (f a)) (hSup : ∀ (s : Set α), (∀ as, p a)p (sSup s)) :
      p (OrderHom.lfp f)
      theorem OrderHom.le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : a f a) :
      a OrderHom.gfp f
      theorem OrderHom.gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : bf b, b a) :
      OrderHom.gfp f a
      theorem OrderHom.isFixedPt_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      Function.IsFixedPt (⇑f) (OrderHom.gfp f)
      @[simp]
      theorem OrderHom.map_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      f (OrderHom.gfp f) = OrderHom.gfp f
      theorem OrderHom.map_le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a OrderHom.gfp f) :
      f a OrderHom.gfp f
      theorem OrderHom.gfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : OrderHom.gfp f a) :
      OrderHom.gfp f f a
      theorem OrderHom.isGreatest_gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :
      IsGreatest {a : α | a f a} (OrderHom.gfp f)
      theorem OrderHom.isGreatest_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
      IsGreatest (Function.fixedPoints f) (OrderHom.gfp f)
      theorem OrderHom.gfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : αProp} (step : ∀ (a : α), p aOrderHom.gfp f ap (f a)) (hInf : ∀ (s : Set α), (∀ as, p a)p (sInf s)) :
      p (OrderHom.gfp f)
      theorem OrderHom.map_lfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :
      f (OrderHom.lfp (g.comp f)) = OrderHom.lfp (f.comp g)
      theorem OrderHom.map_gfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :
      f (OrderHom.gfp (g.comp f)) = OrderHom.gfp (f.comp g)
      theorem OrderHom.lfp_lfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :
      OrderHom.lfp (OrderHom.lfp.comp h) = OrderHom.lfp h.onDiag
      theorem OrderHom.gfp_gfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :
      OrderHom.gfp (OrderHom.gfp.comp h) = OrderHom.gfp h.onDiag
      theorem OrderHom.gfp_const_inf_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) :
      OrderHom.gfp ((OrderHom.const α) x f) x
      def OrderHom.prevFixed {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (hx : f x x) :

      Previous fixed point of a monotone map. If f is a monotone self-map of a complete lattice and x is a point such that f x ≤ x, then f.prevFixed x hx is the greatest fixed point of f that is less than or equal to x.

      Equations
      Instances For
        def OrderHom.nextFixed {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (hx : x f x) :

        Next fixed point of a monotone map. If f is a monotone self-map of a complete lattice and x is a point such that x ≤ f x, then f.nextFixed x hx is the least fixed point of f that is greater than or equal to x.

        Equations
        Instances For
          theorem OrderHom.prevFixed_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) :
          (f.prevFixed x hx) x
          theorem OrderHom.le_nextFixed {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) :
          x (f.nextFixed x hx)
          theorem OrderHom.nextFixed_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) {y : (Function.fixedPoints f)} (h : x y) :
          f.nextFixed x hx y
          @[simp]
          theorem OrderHom.nextFixed_le_iff {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) {y : (Function.fixedPoints f)} :
          f.nextFixed x hx y x y
          @[simp]
          theorem OrderHom.le_prevFixed_iff {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) {y : (Function.fixedPoints f)} :
          y f.prevFixed x hx y x
          theorem OrderHom.le_prevFixed {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) {y : (Function.fixedPoints f)} (h : y x) :
          y f.prevFixed x hx
          theorem OrderHom.le_map_sup_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) (x : (Function.fixedPoints f)) (y : (Function.fixedPoints f)) :
          x y f (x y)
          theorem OrderHom.map_inf_fixedPoints_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : (Function.fixedPoints f)) (y : (Function.fixedPoints f)) :
          f (x y) x y
          theorem OrderHom.le_map_sSup_subset_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) (A : Set α) (hA : A Function.fixedPoints f) :
          sSup A f (sSup A)
          theorem OrderHom.map_sInf_subset_fixedPoints_le {α : Type u} [CompleteLattice α] (f : α →o α) (A : Set α) (hA : A Function.fixedPoints f) :
          f (sInf A) sInf A

          Knaster-Tarski Theorem: The fixed points of f form a complete lattice.

          Equations
          theorem fixedPoints.lfp_eq_sSup_iterate {α : Type u} [CompleteLattice α] (f : α →o α) (h : OmegaCompletePartialOrder.ωScottContinuous f) :
          OrderHom.lfp f = ⨆ (n : ), (⇑f)^[n]

          Kleene's fixed point Theorem: The least fixed point in a complete lattice is the supremum of iterating a function on bottom arbitrary often.

          theorem fixedPoints.gfp_eq_sInf_iterate {α : Type u} [CompleteLattice α] (f : α →o α) (h : OmegaCompletePartialOrder.ωScottContinuous (OrderHom.dual f)) :
          OrderHom.gfp f = ⨅ (n : ), (⇑f)^[n]