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} [inst : CompleteLattice α] :
(α →o α) →o α

Least fixed point of a monotone function

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

Greatest fixed point of a monotone function

Equations
theorem OrderHom.lfp_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (h : f a a) :
OrderHom.lfp f a
theorem OrderHom.lfp_le_fixed {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (h : f a = a) :
OrderHom.lfp f a
theorem OrderHom.le_lfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), f b ba b) :
a OrderHom.lfp f
theorem OrderHom.map_le_lfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (ha : a OrderHom.lfp f) :
f a OrderHom.lfp f
@[simp]
theorem OrderHom.map_lfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
f (OrderHom.lfp f) = OrderHom.lfp f
theorem OrderHom.isFixedPt_lfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
Function.IsFixedPt (f) (OrderHom.lfp f)
theorem OrderHom.lfp_le_map {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (ha : OrderHom.lfp f a) :
OrderHom.lfp f f a
theorem OrderHom.isLeast_lfp_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
IsLeast { a | f a a } (OrderHom.lfp f)
theorem OrderHom.isLeast_lfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
IsLeast (Function.fixedPoints f) (OrderHom.lfp f)
theorem OrderHom.lfp_induction {α : Type u} [inst : CompleteLattice α] (f : α →o α) {p : αProp} (step : (a : α) → p aa OrderHom.lfp fp (f a)) (hSup : (s : Set α) → ((a : α) → a sp a) → p (supₛ s)) :
p (OrderHom.lfp f)
theorem OrderHom.le_gfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (h : a f a) :
a OrderHom.gfp f
theorem OrderHom.gfp_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), b f bb a) :
OrderHom.gfp f a
theorem OrderHom.isFixedPt_gfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
Function.IsFixedPt (f) (OrderHom.gfp f)
@[simp]
theorem OrderHom.map_gfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
f (OrderHom.gfp f) = OrderHom.gfp f
theorem OrderHom.map_le_gfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (ha : a OrderHom.gfp f) :
f a OrderHom.gfp f
theorem OrderHom.gfp_le_map {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α} (ha : OrderHom.gfp f a) :
OrderHom.gfp f f a
theorem OrderHom.isGreatest_gfp_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
IsGreatest { a | a f a } (OrderHom.gfp f)
theorem OrderHom.isGreatest_gfp {α : Type u} [inst : CompleteLattice α] (f : α →o α) :
IsGreatest (Function.fixedPoints f) (OrderHom.gfp f)
theorem OrderHom.gfp_induction {α : Type u} [inst : CompleteLattice α] (f : α →o α) {p : αProp} (step : (a : α) → p aOrderHom.gfp f ap (f a)) (hInf : (s : Set α) → ((a : α) → a sp a) → p (infₛ s)) :
p (OrderHom.gfp f)
theorem OrderHom.map_lfp_comp {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : β →o α) (g : α →o β) :
f (OrderHom.lfp (OrderHom.comp g f)) = OrderHom.lfp (OrderHom.comp f g)
theorem OrderHom.map_gfp_comp {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : β →o α) (g : α →o β) :
f (OrderHom.gfp (OrderHom.comp g f)) = OrderHom.gfp (OrderHom.comp f g)
theorem OrderHom.lfp_lfp {α : Type u} [inst : CompleteLattice α] (h : α →o α →o α) :
OrderHom.lfp (OrderHom.comp OrderHom.lfp h) = OrderHom.lfp (OrderHom.onDiag h)
theorem OrderHom.gfp_gfp {α : Type u} [inst : CompleteLattice α] (h : α →o α →o α) :
OrderHom.gfp (OrderHom.comp OrderHom.gfp h) = OrderHom.gfp (OrderHom.onDiag h)
theorem OrderHom.gfp_const_inf_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : α) :
OrderHom.gfp (↑(OrderHom.const α) x f) x
def OrderHom.prevFixed {α : Type u} [inst : 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≤ x, then f.prevFixed x hx is the greatest fixed point of f that is less than or equal to x.

Equations
def OrderHom.nextFixed {α : Type u} [inst : 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≤ f x, then f.nextFixed x hx is the least fixed point of f that is greater than or equal to x.

Equations
  • One or more equations did not get rendered due to their size.
theorem OrderHom.prevFixed_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) :
↑(OrderHom.prevFixed f x hx) x
theorem OrderHom.le_nextFixed {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) :
x ↑(OrderHom.nextFixed f x hx)
theorem OrderHom.nextFixed_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) {y : ↑(Function.fixedPoints f)} (h : x y) :
@[simp]
theorem OrderHom.nextFixed_le_iff {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x f x) {y : ↑(Function.fixedPoints f)} :
OrderHom.nextFixed f x hx y x y
@[simp]
theorem OrderHom.le_prevFixed_iff {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) {y : ↑(Function.fixedPoints f)} :
y OrderHom.prevFixed f x hx y x
theorem OrderHom.le_prevFixed {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x x) {y : ↑(Function.fixedPoints f)} (h : y x) :
theorem OrderHom.le_map_sup_fixedPoints {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : ↑(Function.fixedPoints f)) (y : ↑(Function.fixedPoints f)) :
x y f (x y)
theorem OrderHom.map_inf_fixedPoints_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x : ↑(Function.fixedPoints f)) (y : ↑(Function.fixedPoints f)) :
f (x y) x y
theorem OrderHom.le_map_supₛ_subset_fixedPoints {α : Type u} [inst : CompleteLattice α] (f : α →o α) (A : Set α) (hA : A Function.fixedPoints f) :
supₛ A f (supₛ A)
theorem OrderHom.map_infₛ_subset_fixedPoints_le {α : Type u} [inst : CompleteLattice α] (f : α →o α) (A : Set α) (hA : A Function.fixedPoints f) :
f (infₛ A) infₛ A
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance fixedPoints.completeLattice {α : Type u} [inst : CompleteLattice α] (f : α →o α) :

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

Equations
  • One or more equations did not get rendered due to their size.