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

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

Least fixed point of a monotone function

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

Greatest fixed point of a monotone function

Equations
source
theorem OrderHom.lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : f a ≤ a) :
lfp f ≤ a
source
theorem OrderHom.lfp_le_fixed {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : f a = a) :
lfp f ≤ a
source
theorem OrderHom.le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), f b ≤ b → a ≤ b) :
a ≤ lfp f
source
theorem OrderHom.map_le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a ≤ lfp f) :
f a ≤ lfp f
source
@[simp]
theorem OrderHom.map_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
f (lfp f) = lfp f
source
theorem OrderHom.isFixedPt_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
Function.IsFixedPt (⇑f) (lfp f)
source
theorem OrderHom.lfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : lfp f ≤ a) :
lfp f ≤ f a
source
theorem OrderHom.isLeast_lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :
IsLeast {a : α | f a ≤ a} (lfp f)
source
theorem OrderHom.isLeast_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :
IsLeast (Function.fixedPoints ⇑f) (lfp f)
source
theorem OrderHom.lfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : α → Prop} (step : ∀ (a : α), p a → a ≤ lfp f → p (f a)) (hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)) :
p (lfp f)
source
theorem OrderHom.le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : a ≤ f a) :
a ≤ gfp f
source
theorem OrderHom.gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ∀ b ≤ f b, b ≤ a) :
gfp f ≤ a
source
theorem OrderHom.isFixedPt_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
Function.IsFixedPt (⇑f) (gfp f)
source
@[simp]
theorem OrderHom.map_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
f (gfp f) = gfp f
source
theorem OrderHom.map_le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a ≤ gfp f) :
f a ≤ gfp f
source
theorem OrderHom.gfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : gfp f ≤ a) :
gfp f ≤ f a
source
theorem OrderHom.isGreatest_gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :
IsGreatest {a : α | a ≤ f a} (gfp f)
source
theorem OrderHom.isGreatest_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :
IsGreatest (Function.fixedPoints ⇑f) (gfp f)
source
theorem OrderHom.gfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : α → Prop} (step : ∀ (a : α), p a → gfp f ≤ a → p (f a)) (hInf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) :
p (gfp f)
source
theorem OrderHom.map_lfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :
f (lfp (g.comp f)) = lfp (f.comp g)
source
theorem OrderHom.map_gfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :
f (gfp (g.comp f)) = gfp (f.comp g)
source
theorem OrderHom.lfp_lfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :
lfp (lfp.comp h) = lfp h.onDiag
source
theorem OrderHom.gfp_gfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :
gfp (gfp.comp h) = gfp h.onDiag
source
theorem OrderHom.gfp_const_inf_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) :
gfp ((const α) x ⊓ f) ≤ x
source
def OrderHom.prevFixed {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (hx : f x ≤ x) :
↑(Function.fixedPoints ⇑f)

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
source
def OrderHom.nextFixed {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) (hx : x ≤ f x) :
↑(Function.fixedPoints ⇑f)

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
source
theorem OrderHom.prevFixed_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x) :
↑(f.prevFixed x hx) ≤ x
source
theorem OrderHom.le_nextFixed {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) :
x ≤ ↑(f.nextFixed x hx)
source
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
source
@[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
source
@[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
source
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
source
theorem OrderHom.le_map_sup_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) (x y : ↑(Function.fixedPoints ⇑f)) :
↑x ⊔ ↑y ≤ f (↑x ⊔ ↑y)
source
theorem OrderHom.map_inf_fixedPoints_le {α : Type u} [CompleteLattice α] (f : α →o α) (x y : ↑(Function.fixedPoints ⇑f)) :
f (↑x ⊓ ↑y) ≤ ↑x ⊓ ↑y
source
theorem OrderHom.le_map_sSup_subset_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) (A : Set α) (hA : A ⊆ Function.fixedPoints ⇑f) :
sSup A ≤ f (sSup A)
source
theorem OrderHom.map_sInf_subset_fixedPoints_le {α : Type u} [CompleteLattice α] (f : α →o α) (A : Set α) (hA : A ⊆ Function.fixedPoints ⇑f) :
f (sInf A) ≤ sInf A
source
instance fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) :
SemilatticeSup ↑(Function.fixedPoints ⇑f)
Equations
source
instance fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) :
SemilatticeInf ↑(Function.fixedPoints ⇑f)
Equations
source
instance fixedPoints.instCompleteSemilatticeSupElemFixedPointsCoeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) :
CompleteSemilatticeSup ↑(Function.fixedPoints ⇑f)
Equations
source
instance fixedPoints.instCompleteSemilatticeInfElemFixedPointsCoeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) :
CompleteSemilatticeInf ↑(Function.fixedPoints ⇑f)
Equations
source
instance fixedPoints.completeLattice {α : Type u} [CompleteLattice α] (f : α →o α) :
CompleteLattice ↑(Function.fixedPoints ⇑f)

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

Equations
source
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.

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