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
Least fixed point of a monotone function
Instances For
Greatest fixed point of a monotone function
Instances For
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
{α : 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 (g.comp f)) = OrderHom.lfp (f.comp g)
theorem
OrderHom.map_gfp_comp
{α : Type u}
{β : Type v}
[CompleteLattice α]
[CompleteLattice β]
(f : β →o α)
(g : α →o β)
:
f (OrderHom.gfp (g.comp f)) = OrderHom.gfp (f.comp g)
theorem
OrderHom.lfp_lfp
{α : Type u}
[CompleteLattice α]
(h : α →o α →o α)
:
OrderHom.lfp (OrderHom.lfp.comp h) = OrderHom.lfp h.onDiag
theorem
OrderHom.gfp_gfp
{α : Type u}
[CompleteLattice α]
(h : α →o α →o α)
:
OrderHom.gfp (OrderHom.gfp.comp h) = OrderHom.gfp h.onDiag
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
- f.prevFixed x hx = ⟨OrderHom.gfp ((OrderHom.const α) x ⊓ f), ⋯⟩
Instances For
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
- f.nextFixed x hx = ⟨OrderHom.lfp ((OrderHom.const α) x ⊔ f), ⋯⟩
Instances For
theorem
OrderHom.prevFixed_le
{α : Type u}
[CompleteLattice α]
(f : α →o α)
{x : α}
(hx : f x ≤ x)
:
↑(f.prevFixed x hx) ≤ x
theorem
OrderHom.le_nextFixed
{α : Type u}
[CompleteLattice α]
(f : α →o α)
{x : α}
(hx : x ≤ f x)
:
x ≤ ↑(f.nextFixed x hx)
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
@[simp]
theorem
OrderHom.nextFixed_le_iff
{α : Type u}
[CompleteLattice α]
(f : α →o α)
{x : α}
(hx : x ≤ f x)
{y : ↑(Function.fixedPoints ⇑f)}
:
@[simp]
theorem
OrderHom.le_prevFixed_iff
{α : Type u}
[CompleteLattice α]
(f : α →o α)
{x : α}
(hx : f x ≤ x)
{y : ↑(Function.fixedPoints ⇑f)}
:
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
theorem
OrderHom.le_map_sup_fixedPoints
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(x y : ↑(Function.fixedPoints ⇑f))
:
theorem
OrderHom.map_inf_fixedPoints_le
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(x y : ↑(Function.fixedPoints ⇑f))
:
theorem
OrderHom.le_map_sSup_subset_fixedPoints
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(A : Set α)
(hA : A ⊆ Function.fixedPoints ⇑f)
:
theorem
OrderHom.map_sInf_subset_fixedPoints_le
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(A : Set α)
(hA : A ⊆ Function.fixedPoints ⇑f)
:
instance
fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHom
{α : Type u}
[CompleteLattice α]
(f : α →o α)
:
Equations
- fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHom f = SemilatticeSup.mk (fun (x y : ↑(Function.fixedPoints ⇑f)) => f.nextFixed (↑x ⊔ ↑y) ⋯) ⋯ ⋯ ⋯
instance
fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHom
{α : Type u}
[CompleteLattice α]
(f : α →o α)
:
Equations
- fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHom f = SemilatticeInf.mk (fun (x y : ↑(Function.fixedPoints ⇑f)) => f.prevFixed (↑x ⊓ ↑y) ⋯) ⋯ ⋯ ⋯
instance
fixedPoints.instCompleteSemilatticeSupElemFixedPointsCoeOrderHom
{α : Type u}
[CompleteLattice α]
(f : α →o α)
:
instance
fixedPoints.instCompleteSemilatticeInfElemFixedPointsCoeOrderHom
{α : Type u}
[CompleteLattice α]
(f : α →o α)
:
Knaster-Tarski Theorem: The fixed points of f form a complete lattice.
Equations
- fixedPoints.completeLattice f = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
fixedPoints.lfp_eq_sSup_iterate
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(h : OmegaCompletePartialOrder.ωScottContinuous ⇑f)
:
Kleene's fixed point Theorem: The least fixed point in a complete lattice is the supremum of iterating a function on bottom arbitrary often.
theorem
fixedPoints.gfp_eq_sInf_iterate
{α : Type u}
[CompleteLattice α]
(f : α →o α)
(h : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual f))
: