mathlib documentation

order.fixed_points

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 lfp {α : Type u} [complete_lattice α] (f : α → α) :
α

Least fixed point of a monotone function

Equations
def gfp {α : Type u} [complete_lattice α] (f : α → α) :
α

Greatest fixed point of a monotone function

Equations
theorem lfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : f a a) :
lfp f a
theorem le_lfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : ∀ (b : α), f b ba b) :
a lfp f
theorem lfp_fixed_point {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) :
f (lfp f) = lfp f
theorem lfp_induction {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} (hf : monotone f) (step : ∀ (a : α), p aa lfp fp (f a)) (hSup : ∀ (s : set α), (∀ (a : α), a sp a)p (Sup s)) :
p (lfp f)
theorem monotone_lfp {α : Type u} [complete_lattice α] :
theorem le_gfp {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : a f a) :
a gfp f
theorem gfp_le {α : Type u} [complete_lattice α] {f : α → α} {a : α} (h : ∀ (b : α), b f bb a) :
gfp f a
theorem gfp_fixed_point {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) :
f (gfp f) = gfp f
theorem gfp_induction {α : Type u} [complete_lattice α] {f : α → α} {p : α → Prop} (hf : monotone f) (step : ∀ (a : α), p agfp f ap (f a)) (hInf : ∀ (s : set α), (∀ (a : α), a sp a)p (Inf s)) :
p (gfp f)
theorem monotone_gfp {α : Type u} [complete_lattice α] :
theorem lfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} (hf : monotone f) (hg : monotone g) :
lfp (f g) = f (lfp (g f))
theorem gfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β} (hf : monotone f) (hg : monotone g) :
gfp (f g) = f (gfp (g f))
theorem lfp_lfp {α : Type u} [complete_lattice α] {h : α → α → α} (m : ∀ ⦃a b c d : α⦄, a bc dh a c h b d) :
lfp (lfp h) = lfp (λ (x : α), h x x)
theorem gfp_gfp {α : Type u} [complete_lattice α] {h : α → α → α} (m : ∀ ⦃a b c d : α⦄, a bc dh a c h b d) :
gfp (gfp h) = gfp (λ (x : α), h x x)
def fixed_points.prev {α : Type u} [complete_lattice α] (f : α → α) (x : α) :
α
Equations
def fixed_points.next {α : Type u} [complete_lattice α] (f : α → α) (x : α) :
α
Equations
theorem fixed_points.prev_le {α : Type u} [complete_lattice α] {f : α → α} {x : α} :
theorem fixed_points.prev_eq {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) {a : α} (h : f a a) :
def fixed_points.prev_fixed {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) (a : α) (h : f a a) :
Equations
theorem fixed_points.le_next {α : Type u} [complete_lattice α] {f : α → α} {x : α} :
theorem fixed_points.next_eq {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) {a : α} (h : a f a) :
def fixed_points.next_fixed {α : Type u} [complete_lattice α] {f : α → α} (hf : monotone f) (a : α) (h : a f a) :
Equations
theorem fixed_points.sup_le_f_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (x y : (function.fixed_points f)) :
x.val y.val f (x.val y.val)
theorem fixed_points.f_le_inf_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (x y : (function.fixed_points f)) :
f (x.val y.val) x.val y.val
theorem fixed_points.Sup_le_f_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) (hA : A function.fixed_points f) :
Sup A f (Sup A)
theorem fixed_points.f_le_Inf_of_fixed_points {α : Type u} [complete_lattice α] (f : α → α) (hf : monotone f) (A : set α) (hA : A function.fixed_points f) :
f (Inf A) Inf A

Knaster-Tarski Theorem: The fixed points of f form a complete lattice. This cannot be an instance, since it depends on the monotonicity of f.

Equations