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

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' := ⋯ }

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' := ⋯ }

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 ≤ b → a ≤ 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 a → a ≤ OrderHom.lfp f → p (f a)) (hSup : ∀ (s : Set α), (∀ a ∈ s, 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 : ∀ b ≤ f 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 a → OrderHom.gfp f ≤ a → p (f a)) (hInf : ∀ (s : Set α), (∀ a ∈ s, 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 (OrderHom.comp g f)) = OrderHom.lfp (OrderHom.comp f g)

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)

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

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

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) : ↑(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 := ⋯ }

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

• OrderHom.nextFixed f x hx = let __src := OrderHom.prevFixed (OrderHom.dual f) x hx; { val := OrderHom.lfp ((OrderHom.const α) x ⊔ f), property := ⋯ }

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

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

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

@[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

@[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

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

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

instance fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfInstFunLikeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) : SemilatticeSup ↑(Function.fixedPoints ⇑f)

Equations

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

instance fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfInstFunLikeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) : SemilatticeInf ↑(Function.fixedPoints ⇑f)

Equations

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

instance fixedPoints.instCompleteSemilatticeSupElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfInstFunLikeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) : CompleteSemilatticeSup ↑(Function.fixedPoints ⇑f)

Equations

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

instance fixedPoints.instCompleteSemilatticeInfElemFixedPointsCoeOrderHomToPreorderToPartialOrderToCompleteSemilatticeInfInstFunLikeOrderHom {α : Type u} [CompleteLattice α] (f : α →o α) : CompleteSemilatticeInf ↑(Function.fixedPoints ⇑f)

Equations

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

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.