mathlib3 documentation

order.fixed_points

Fixed point construction on complete lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Least fixed point of a monotone function

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

Greatest fixed point of a monotone function

Equations
source
theorem order_hom.lfp_le {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (h : ⇑f a ≤ a) :
⇑order_hom.lfp f ≤ a
source
theorem order_hom.lfp_le_fixed {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (h : ⇑f a = a) :
⇑order_hom.lfp f ≤ a
source
theorem order_hom.le_lfp {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (h : ∀ (b : α), ⇑f b ≤ b → a ≤ b) :
a ≤ ⇑order_hom.lfp f
source
theorem order_hom.map_le_lfp {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (ha : a ≤ ⇑order_hom.lfp f) :
⇑f a ≤ ⇑order_hom.lfp f
source
@[simp]
theorem order_hom.map_lfp {α : Type u} [complete_lattice α] (f : α →o α) :
⇑f (⇑order_hom.lfp f) = ⇑order_hom.lfp f
source
theorem order_hom.is_fixed_pt_lfp {α : Type u} [complete_lattice α] (f : α →o α) :
function.is_fixed_pt ⇑f (⇑order_hom.lfp f)
source
theorem order_hom.lfp_le_map {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (ha : ⇑order_hom.lfp f ≤ a) :
⇑order_hom.lfp f ≤ ⇑f a
source
theorem order_hom.is_least_lfp_le {α : Type u} [complete_lattice α] (f : α →o α) :
is_least {a : α | ⇑f a ≤ a} (⇑order_hom.lfp f)
source
theorem order_hom.is_least_lfp {α : Type u} [complete_lattice α] (f : α →o α) :
is_least (function.fixed_points ⇑f) (⇑order_hom.lfp f)
source
theorem order_hom.lfp_induction {α : Type u} [complete_lattice α] (f : α →o α) {p : α → Prop} (step : ∀ (a : α), p a → a ≤ ⇑order_hom.lfp f → p (⇑f a)) (hSup : ∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (has_Sup.Sup s)) :
p (⇑order_hom.lfp f)
source
theorem order_hom.le_gfp {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (h : a ≤ ⇑f a) :
a ≤ ⇑order_hom.gfp f
source
theorem order_hom.gfp_le {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (h : ∀ (b : α), b ≤ ⇑f b → b ≤ a) :
⇑order_hom.gfp f ≤ a
source
theorem order_hom.is_fixed_pt_gfp {α : Type u} [complete_lattice α] (f : α →o α) :
function.is_fixed_pt ⇑f (⇑order_hom.gfp f)
source
@[simp]
theorem order_hom.map_gfp {α : Type u} [complete_lattice α] (f : α →o α) :
⇑f (⇑order_hom.gfp f) = ⇑order_hom.gfp f
source
theorem order_hom.map_le_gfp {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (ha : a ≤ ⇑order_hom.gfp f) :
⇑f a ≤ ⇑order_hom.gfp f
source
theorem order_hom.gfp_le_map {α : Type u} [complete_lattice α] (f : α →o α) {a : α} (ha : ⇑order_hom.gfp f ≤ a) :
⇑order_hom.gfp f ≤ ⇑f a
source
theorem order_hom.is_greatest_gfp_le {α : Type u} [complete_lattice α] (f : α →o α) :
is_greatest {a : α | a ≤ ⇑f a} (⇑order_hom.gfp f)
source
theorem order_hom.is_greatest_gfp {α : Type u} [complete_lattice α] (f : α →o α) :
is_greatest (function.fixed_points ⇑f) (⇑order_hom.gfp f)
source
theorem order_hom.gfp_induction {α : Type u} [complete_lattice α] (f : α →o α) {p : α → Prop} (step : ∀ (a : α), p a → ⇑order_hom.gfp f ≤ a → p (⇑f a)) (hInf : ∀ (s : set α), (∀ (a : α), a ∈ s → p a) → p (has_Inf.Inf s)) :
p (⇑order_hom.gfp f)
source
theorem order_hom.map_lfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] (f : β →o α) (g : α →o β) :
⇑f (⇑order_hom.lfp (g.comp f)) = ⇑order_hom.lfp (f.comp g)
source
theorem order_hom.map_gfp_comp {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] (f : β →o α) (g : α →o β) :
⇑f (⇑order_hom.gfp (g.comp f)) = ⇑order_hom.gfp (f.comp g)
source
theorem order_hom.lfp_lfp {α : Type u} [complete_lattice α] (h : α →o α →o α) :
⇑order_hom.lfp (order_hom.lfp.comp h) = ⇑order_hom.lfp h.on_diag
source
theorem order_hom.gfp_gfp {α : Type u} [complete_lattice α] (h : α →o α →o α) :
⇑order_hom.gfp (order_hom.gfp.comp h) = ⇑order_hom.gfp h.on_diag
source
theorem order_hom.gfp_const_inf_le {α : Type u} [complete_lattice α] (f : α →o α) (x : α) :
⇑order_hom.gfp (⇑(order_hom.const α) x ⊓ f) ≤ x
source
def order_hom.prev_fixed {α : Type u} [complete_lattice α] (f : α →o α) (x : α) (hx : ⇑f x ≤ x) :
↥(function.fixed_points ⇑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.prev_fixed x hx is the greatest fixed point of f that is less than or equal to x.

Equations
source
def order_hom.next_fixed {α : Type u} [complete_lattice α] (f : α →o α) (x : α) (hx : x ≤ ⇑f x) :
↥(function.fixed_points ⇑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.next_fixed x hx is the least fixed point of f that is greater than or equal to x.

Equations
source
theorem order_hom.prev_fixed_le {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : ⇑f x ≤ x) :
↑(f.prev_fixed x hx) ≤ x
source
theorem order_hom.le_next_fixed {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : x ≤ ⇑f x) :
x ≤ ↑(f.next_fixed x hx)
source
theorem order_hom.next_fixed_le {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : x ≤ ⇑f x) {y : ↥(function.fixed_points ⇑f)} (h : x ≤ ↑y) :
f.next_fixed x hx ≤ y
source
@[simp]
theorem order_hom.next_fixed_le_iff {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : x ≤ ⇑f x) {y : ↥(function.fixed_points ⇑f)} :
f.next_fixed x hx ≤ y ↔ x ≤ ↑y
source
@[simp]
theorem order_hom.le_prev_fixed_iff {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : ⇑f x ≤ x) {y : ↥(function.fixed_points ⇑f)} :
y ≤ f.prev_fixed x hx ↔ ↑y ≤ x
source
theorem order_hom.le_prev_fixed {α : Type u} [complete_lattice α] (f : α →o α) {x : α} (hx : ⇑f x ≤ x) {y : ↥(function.fixed_points ⇑f)} (h : ↑y ≤ x) :
y ≤ f.prev_fixed x hx
source
theorem order_hom.le_map_sup_fixed_points {α : Type u} [complete_lattice α] (f : α →o α) (x y : ↥(function.fixed_points ⇑f)) :
↑x ⊔ ↑y ≤ ⇑f (↑x ⊔ ↑y)
source
theorem order_hom.map_inf_fixed_points_le {α : Type u} [complete_lattice α] (f : α →o α) (x y : ↥(function.fixed_points ⇑f)) :
⇑f (↑x ⊓ ↑y) ≤ ↑x ⊓ ↑y
source
theorem order_hom.le_map_Sup_subset_fixed_points {α : Type u} [complete_lattice α] (f : α →o α) (A : set α) (hA : A ⊆ function.fixed_points ⇑f) :
has_Sup.Sup A ≤ ⇑f (has_Sup.Sup A)
source
theorem order_hom.map_Inf_subset_fixed_points_le {α : Type u} [complete_lattice α] (f : α →o α) (A : set α) (hA : A ⊆ function.fixed_points ⇑f) :
⇑f (has_Inf.Inf A) ≤ has_Inf.Inf A
source
@[protected, instance]
def fixed_points.function.fixed_points.semilattice_sup {α : Type u} [complete_lattice α] (f : α →o α) :
semilattice_sup ↥(function.fixed_points ⇑f)
Equations
source
@[protected, instance]
def fixed_points.function.fixed_points.semilattice_inf {α : Type u} [complete_lattice α] (f : α →o α) :
semilattice_inf ↥(function.fixed_points ⇑f)
Equations
source
@[protected, instance]
def fixed_points.function.fixed_points.complete_semilattice_Sup {α : Type u} [complete_lattice α] (f : α →o α) :
complete_semilattice_Sup ↥(function.fixed_points ⇑f)
Equations
source
@[protected, instance]
def fixed_points.function.fixed_points.complete_semilattice_Inf {α : Type u} [complete_lattice α] (f : α →o α) :
complete_semilattice_Inf ↥(function.fixed_points ⇑f)
Equations
source
@[protected, instance]
def fixed_points.function.fixed_points.complete_lattice {α : Type u} [complete_lattice α] (f : α →o α) :
complete_lattice ↥(function.fixed_points ⇑f)

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

Equations