Documentation

WGCL.FixedPoints

@[reducible, inline]

abbrev OmegaCompletePartialOrder.iterate_bot {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) :

Equations

OmegaCompletePartialOrder.iterate_bot f = { toFun := fun (x : ℕ) => (⇑f)^[x] ⊥, monotone' := ⋯ }

Instances For

def OmegaCompletePartialOrder.lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] :

(α →o α) →o α

Equations

OmegaCompletePartialOrder.lfp = { toFun := fun (f : α →o α) => OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.iterate_bot f), monotone' := ⋯ }

Instances For

theorem OmegaCompletePartialOrder.lfp_le {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) {a : α} (h : f a ≤ a) :

theorem OmegaCompletePartialOrder.lfp_le_fixed {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) {a : α} (h : f a = a) :

theorem OmegaCompletePartialOrder.lfp_le_map {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) :

lfp f ≤ f (lfp f)

theorem OmegaCompletePartialOrder.le_lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) {a : α} (hf : ωScottContinuous ⇑f) (h : ∀ (b : α), f b ≤ b → a ≤ b) :

theorem OmegaCompletePartialOrder.map_le_lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) {a : α} (hf : ωScottContinuous ⇑f) (h : a ≤ lfp f) :

f a ≤ lfp f

theorem OmegaCompletePartialOrder.map_lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) (hf : ωScottContinuous ⇑f) :

f (lfp f) = lfp f

theorem OmegaCompletePartialOrder.isFixedPt_lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) (hf : ωScottContinuous ⇑f) :

Function.IsFixedPt (⇑f) (lfp f)

theorem OmegaCompletePartialOrder.isLeast_lfp_le {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) (hf : ωScottContinuous ⇑f) :

IsLeast {a : α | f a ≤ a} (lfp f)

theorem OmegaCompletePartialOrder.isLeast_lfp {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] (f : α →o α) (hf : ωScottContinuous ⇑f) :

IsLeast (Function.fixedPoints ⇑f) (lfp f)

theorem OmegaCompletePartialOrder.lfp.ωScottContinuous {α : Type u_1} [instOrder : OmegaCompletePartialOrder α] [OrderBot α] :

OmegaCompletePartialOrder.ωScottContinuous ⇑lfp

@[reducible, inline]

abbrev OmegaCompletePartialOrder.iterate_top {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) :

OrderDualHom ℕ α

Equations

OmegaCompletePartialOrder.iterate_top f = { toFun := fun (x : ℕ) => (⇑f)^[x] ⊤, antitone' := ⋯ }

Instances For

theorem OmegaCompletePartialOrder.iterate_top.mono {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] :

Monotone iterate_top

def OmegaCompletePartialOrder.gfp {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] :

(α →o α) →o α

Equations

OmegaCompletePartialOrder.gfp = { toFun := fun (f : α →o α) => OmegaCompletePartialOrderBi.ωInf (OmegaCompletePartialOrder.iterate_top f), monotone' := ⋯ }

Instances For

theorem OmegaCompletePartialOrder.le_gfp {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] {a : α} (h : a ≤ f a) :

@[simp]

theorem OmegaCompletePartialOrder.iterate_top_apply {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] {i : ℕ} :

(iterate_top f) i = (⇑f)^[i] ⊤

theorem OmegaCompletePartialOrder.gfp_le {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] {a : α} (h : ∀ b ≤ f b, b ≤ a) :

theorem OmegaCompletePartialOrder.isFixedPt_gfp {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] :

Function.IsFixedPt (⇑f) (gfp f)

theorem OmegaCompletePartialOrder.map_gfp {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] :

f (gfp f) = gfp f

theorem OmegaCompletePartialOrder.gfp_le_map {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] {a : α} (ha : gfp f ≤ a) :

gfp f ≤ f a

theorem OmegaCompletePartialOrder.isGreatest_gfp_le {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] :

IsGreatest {a : α | a ≤ f a} (gfp f)

theorem OmegaCompletePartialOrder.isGreatest_gfp {α : Type} [OmegaCompletePartialOrder α] [OrderTop α] (f : α →o α) [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrderBi α] :

IsGreatest (Function.fixedPoints ⇑f) (gfp f)