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 #

OrderHom.lfp: The least fixed point of a bundled monotone function.
OrderHom.gfp: The greatest fixed point of a bundled monotone function.
OrderHom.prevFixed: The greatest fixed point of a bundled monotone function smaller than or equal to a given element.
OrderHom.nextFixed: The least fixed point of a bundled monotone function greater than or equal to a given element.
fixedPoints.completeLattice: The Knaster-Tarski theorem: fixed points of a monotone self-map of a complete lattice form themselves a complete lattice.

Tags #

fixed point, complete lattice, monotone function

source

def OrderHom.lfp {α : Type u} [CompleteLattice α] :

(α →o α) →o α

Least fixed point of a monotone function

Equations

OrderHom.lfp = { toFun := fun f => sInf {a | ↑f a ≤ a}, monotone' := (_ : ∀ (x x_1 : α →o α), x ≤ x_1 → sInf {a | ↑x a ≤ a} ≤ sInf {a | ↑x_1 a ≤ a}) }

Instances For

source

def OrderHom.gfp {α : Type u} [CompleteLattice α] :

(α →o α) →o α

Greatest fixed point of a monotone function

Equations

OrderHom.gfp = { toFun := fun f => sSup {a | a ≤ ↑f a}, monotone' := (_ : ∀ (x x_1 : α →o α), x ≤ x_1 → sSup {a | a ≤ ↑x a} ≤ sSup {a | a ≤ ↑x_1 a}) }

Instances For

source

theorem OrderHom.lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ↑f a ≤ a) :

↑OrderHom.lfp f ≤ a

source

theorem OrderHom.lfp_le_fixed {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ↑f a = a) :

↑OrderHom.lfp f ≤ a

source

theorem OrderHom.le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), ↑f b ≤ b → a ≤ b) :

a ≤ ↑OrderHom.lfp f

source

theorem OrderHom.map_le_lfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a ≤ ↑OrderHom.lfp f) :

↑f a ≤ ↑OrderHom.lfp f

source

@[simp]

theorem OrderHom.map_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :

↑f (↑OrderHom.lfp f) = ↑OrderHom.lfp f

source

theorem OrderHom.isFixedPt_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :

Function.IsFixedPt (↑f) (↑OrderHom.lfp f)

source

theorem OrderHom.lfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : ↑OrderHom.lfp f ≤ a) :

↑OrderHom.lfp f ≤ ↑f a

source

theorem OrderHom.isLeast_lfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :

IsLeast {a | ↑f a ≤ a} (↑OrderHom.lfp f)

source

theorem OrderHom.isLeast_lfp {α : Type u} [CompleteLattice α] (f : α →o α) :

IsLeast (Function.fixedPoints ↑f) (↑OrderHom.lfp f)

source

theorem OrderHom.lfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : α → Prop} (step : (a : α) → p a → a ≤ ↑OrderHom.lfp f → p (↑f a)) (hSup : (s : Set α) → ((a : α) → a ∈ s → p a) → p (sSup s)) :

p (↑OrderHom.lfp f)

source

theorem OrderHom.le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : a ≤ ↑f a) :

a ≤ ↑OrderHom.gfp f

source

theorem OrderHom.gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (h : ∀ (b : α), b ≤ ↑f b → b ≤ a) :

↑OrderHom.gfp f ≤ a

source

theorem OrderHom.isFixedPt_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :

Function.IsFixedPt (↑f) (↑OrderHom.gfp f)

source

@[simp]

theorem OrderHom.map_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :

↑f (↑OrderHom.gfp f) = ↑OrderHom.gfp f

source

theorem OrderHom.map_le_gfp {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : a ≤ ↑OrderHom.gfp f) :

↑f a ≤ ↑OrderHom.gfp f

source

theorem OrderHom.gfp_le_map {α : Type u} [CompleteLattice α] (f : α →o α) {a : α} (ha : ↑OrderHom.gfp f ≤ a) :

↑OrderHom.gfp f ≤ ↑f a

source

theorem OrderHom.isGreatest_gfp_le {α : Type u} [CompleteLattice α] (f : α →o α) :

IsGreatest {a | a ≤ ↑f a} (↑OrderHom.gfp f)

source

theorem OrderHom.isGreatest_gfp {α : Type u} [CompleteLattice α] (f : α →o α) :

IsGreatest (Function.fixedPoints ↑f) (↑OrderHom.gfp f)

source

theorem OrderHom.gfp_induction {α : Type u} [CompleteLattice α] (f : α →o α) {p : α → Prop} (step : (a : α) → p a → ↑OrderHom.gfp f ≤ a → p (↑f a)) (hInf : (s : Set α) → ((a : α) → a ∈ s → p a) → p (sInf s)) :

p (↑OrderHom.gfp f)

source

theorem OrderHom.map_lfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :

↑f (↑OrderHom.lfp (OrderHom.comp g f)) = ↑OrderHom.lfp (OrderHom.comp f g)

source

theorem OrderHom.map_gfp_comp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β) :

↑f (↑OrderHom.gfp (OrderHom.comp g f)) = ↑OrderHom.gfp (OrderHom.comp f g)

source

theorem OrderHom.lfp_lfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :

↑OrderHom.lfp (OrderHom.comp OrderHom.lfp h) = ↑OrderHom.lfp (OrderHom.onDiag h)

source

theorem OrderHom.gfp_gfp {α : Type u} [CompleteLattice α] (h : α →o α →o α) :

↑OrderHom.gfp (OrderHom.comp OrderHom.gfp h) = ↑OrderHom.gfp (OrderHom.onDiag h)

source

theorem OrderHom.gfp_const_inf_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) :

↑OrderHom.gfp (↑(OrderHom.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

OrderHom.prevFixed f x hx = { val := ↑OrderHom.gfp (↑(OrderHom.const α) x ⊓ f), property := (_ : ↑f (↑OrderHom.gfp (↑(OrderHom.const α) x ⊓ f)) = ↑OrderHom.gfp (↑(OrderHom.const α) x ⊓ f)) }

Instances For

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

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

Instances For

source

theorem OrderHom.prevFixed_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : ↑f x ≤ x) :

↑(OrderHom.prevFixed f x hx) ≤ x

source

theorem OrderHom.le_nextFixed {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ ↑f x) :

x ≤ ↑(OrderHom.nextFixed f x hx)

source

theorem OrderHom.nextFixed_le {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ ↑f x) {y : ↑(Function.fixedPoints ↑f)} (h : x ≤ ↑y) :

OrderHom.nextFixed f x hx ≤ y

source

@[simp]

theorem OrderHom.nextFixed_le_iff {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ ↑f x) {y : ↑(Function.fixedPoints ↑f)} :

OrderHom.nextFixed f 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 ≤ OrderHom.prevFixed f 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 ≤ OrderHom.prevFixed f x hx

source

theorem OrderHom.le_map_sup_fixedPoints {α : Type u} [CompleteLattice α] (f : α →o α) (x : ↑(Function.fixedPoints ↑f)) (y : ↑(Function.fixedPoints ↑f)) :

↑x ⊔ ↑y ≤ ↑f (↑x ⊔ ↑y)

source

theorem OrderHom.map_inf_fixedPoints_le {α : Type u} [CompleteLattice α] (f : α →o α) (x : ↑(Function.fixedPoints ↑f)) (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.instSemilatticeSupElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfToFunLikeLeToLEInstOrderHomClassOrderHomToLEToLE {α : Type u} [CompleteLattice α] (f : α →o α) :

SemilatticeSup ↑(Function.fixedPoints ↑f)

Equations

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

source

instance fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfToFunLikeLeToLEInstOrderHomClassOrderHomToLEToLE {α : Type u} [CompleteLattice α] (f : α →o α) :

SemilatticeInf ↑(Function.fixedPoints ↑f)

Equations

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

source

instance fixedPoints.instCompleteSemilatticeSupElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfToFunLikeLeToLEInstOrderHomClassOrderHomToLEToLE {α : Type u} [CompleteLattice α] (f : α →o α) :

CompleteSemilatticeSup ↑(Function.fixedPoints ↑f)

Equations

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

source

instance fixedPoints.instCompleteSemilatticeInfElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfToFunLikeLeToLEInstOrderHomClassOrderHomToLEToLE {α : Type u} [CompleteLattice α] (f : α →o α) :

CompleteSemilatticeInf ↑(Function.fixedPoints ↑f)

Equations

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

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

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