Mathlib.Order.FixedPoints

OrderHom.lfp definition

: (α →o α) →o α

Full source

/-- Least fixed point of a monotone function -/
def lfp : (α →o α) →o α where
  toFun f := sInf { a | f a ≤ a }
  monotone' _ _ hle := sInf_le_sInf fun a ha => (hle a).trans ha

Least fixed point of a monotone function

Informal description

The least fixed point of a monotone function $f$ on a complete lattice $\alpha$ is defined as the infimum of all elements $a \in \alpha$ such that $f(a) \leq a$. This construction yields the smallest element $x$ satisfying $x = f(x)$.

OrderHom.gfp definition

: (α →o α) →o α

Full source

/-- Greatest fixed point of a monotone function -/
def gfp : (α →o α) →o α where
  toFun f := sSup { a | a ≤ f a }
  monotone' _ _ hle := sSup_le_sSup fun a ha => le_trans ha (hle a)

Greatest fixed point of a monotone function

Informal description

The greatest fixed point of a monotone function $f$ on a complete lattice $\alpha$ is defined as the supremum of all elements $a \in \alpha$ such that $a \leq f(a)$. This construction yields the largest element $x$ satisfying $x = f(x)$.

OrderHom.lfp_le theorem

{a : α} (h : f a ≤ a) : f.lfp ≤ a

Full source

theorem lfp_le {a : α} (h : f a ≤ a) : f.lfp ≤ a :=
  sInf_le h

Least Fixed Point is Below Any Prefixed Point

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f : \alpha \to \alpha$, if $f(a) \leq a$, then the least fixed point of $f$ satisfies $\text{lfp}(f) \leq a$.

OrderHom.lfp_le_fixed theorem

{a : α} (h : f a = a) : f.lfp ≤ a

Full source

theorem lfp_le_fixed {a : α} (h : f a = a) : f.lfp ≤ a :=
  f.lfp_le h.le

Least Fixed Point is Below Any Fixed Point

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f : \alpha \to \alpha$, if $a$ is a fixed point of $f$ (i.e., $f(a) = a$), then the least fixed point of $f$ satisfies $\text{lfp}(f) \leq a$.

OrderHom.le_lfp theorem

{a : α} (h : ∀ b, f b ≤ b → a ≤ b) : a ≤ f.lfp

Full source

theorem le_lfp {a : α} (h : ∀ b, f b ≤ b → a ≤ b) : a ≤ f.lfp :=
  le_sInf h

Lower Bound Condition Implies Inequality with Least Fixed Point

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f : \alpha \to \alpha$, if $a$ is a lower bound for all elements $b$ satisfying $f(b) \leq b$, then $a$ is less than or equal to the least fixed point of $f$, i.e., $a \leq \text{lfp}(f)$.

OrderHom.map_le_lfp theorem

{a : α} (ha : a ≤ f.lfp) : f a ≤ f.lfp

Full source

theorem map_le_lfp {a : α} (ha : a ≤ f.lfp) : f a ≤ f.lfp :=
  f.le_lfp fun _ hb => (f.mono <| le_sInf_iff.1 ha _ hb).trans hb

Monotonicity Preserves Least Fixed Point Bound: $a \leq \text{lfp}(f) \Rightarrow f(a) \leq \text{lfp}(f)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f \colon \alpha \to \alpha$, if $a \leq \text{lfp}(f)$, then $f(a) \leq \text{lfp}(f)$, where $\text{lfp}(f)$ denotes the least fixed point of $f$.

OrderHom.map_lfp theorem

: f f.lfp = f.lfp

Full source

@[simp]
theorem map_lfp : f f.lfp = f.lfp :=
  have h : f f.lfp ≤ f.lfp := f.map_le_lfp le_rfl
  h.antisymm <| f.lfp_le <| f.mono h

Least Fixed Point Property: $f(\text{lfp}(f)) = \text{lfp}(f)$

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the least fixed point $\text{lfp}(f)$ satisfies $f(\text{lfp}(f)) = \text{lfp}(f)$.

OrderHom.isFixedPt_lfp theorem

: IsFixedPt f f.lfp

Full source

theorem isFixedPt_lfp : IsFixedPt f f.lfp :=
  f.map_lfp

Least Fixed Point Property: $f(\text{lfp}(f)) = \text{lfp}(f)$

Informal description

The least fixed point $\text{lfp}(f)$ of a monotone function $f$ on a complete lattice is indeed a fixed point of $f$, i.e., $f(\text{lfp}(f)) = \text{lfp}(f)$.

OrderHom.lfp_le_map theorem

{a : α} (ha : f.lfp ≤ a) : f.lfp ≤ f a

Full source

theorem lfp_le_map {a : α} (ha : f.lfp ≤ a) : f.lfp ≤ f a :=
  calc
    f.lfp = f f.lfp := f.map_lfp.symm
    _ ≤ f a := f.mono ha

Monotonicity Inequality for Least Fixed Points: $\text{lfp}(f) \leq a \implies \text{lfp}(f) \leq f(a)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f \colon \alpha \to \alpha$, if the least fixed point $\text{lfp}(f)$ of $f$ satisfies $\text{lfp}(f) \leq a$, then $\text{lfp}(f) \leq f(a)$.

OrderHom.isLeast_lfp_le theorem

: IsLeast {a | f a ≤ a} f.lfp

Full source

theorem isLeast_lfp_le : IsLeast { a | f a ≤ a } f.lfp :=
  ⟨f.map_lfp.le, fun _ => f.lfp_le⟩

Least Fixed Point is the Least Prefixed Point

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the least fixed point $\text{lfp}(f)$ is the least element of the set $\{a \in \alpha \mid f(a) \leq a\}$.

OrderHom.isLeast_lfp theorem

: IsLeast (fixedPoints f) f.lfp

Full source

theorem isLeast_lfp : IsLeast (fixedPoints f) f.lfp :=
  ⟨f.isFixedPt_lfp, fun _ => f.lfp_le_fixed⟩

Least Fixed Point is the Least Element of Fixed Points

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the least fixed point $\mathrm{lfp}(f)$ is the least element of the set of fixed points of $f$, i.e., $\mathrm{lfp}(f)$ is a fixed point of $f$ and for any other fixed point $a$ of $f$, we have $\mathrm{lfp}(f) \leq a$.

OrderHom.lfp_induction theorem

 {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p (f a)) (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) : p f.lfp

Full source

theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p (f a))
    (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) : p f.lfp := by
  set s := { a | a ≤ f.lfp ∧ p a }
  specialize hSup s fun a => And.right
  suffices sSup s = f.lfp from this ▸ hSup
  have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
  have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
  exact h.antisymm (f.lfp_le <| le_sSup hmem)

Induction Principle for Least Fixed Points in Complete Lattices

Informal description

Let $f$ be a monotone function on a complete lattice $\alpha$, and let $\text{lfp}(f)$ be its least fixed point. For any predicate $p$ on $\alpha$, if: 1. For every $a \in \alpha$, if $p(a)$ holds and $a \leq \text{lfp}(f)$, then $p(f(a))$ holds, and 2. For every subset $s \subseteq \alpha$, if $p(a)$ holds for all $a \in s$, then $p(\sup s)$ holds, then $p(\text{lfp}(f))$ holds.

OrderHom.le_gfp theorem

{a : α} (h : a ≤ f a) : a ≤ f.gfp

Full source

theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ f.gfp :=
  le_sSup h

Element Below Fixed Point is Below Greatest Fixed Point

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f : \alpha \to \alpha$, if $a \leq f(a)$, then $a$ is less than or equal to the greatest fixed point of $f$, denoted $\mathrm{gfp}(f)$.

OrderHom.gfp_le theorem

{a : α} (h : ∀ b, b ≤ f b → b ≤ a) : f.gfp ≤ a

Full source

theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : f.gfp ≤ a :=
  sSup_le h

Greatest Fixed Point is Least Upper Bound of Pre-Fixed Points

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f : \alpha \to \alpha$, if every element $b \in \alpha$ satisfying $b \leq f(b)$ also satisfies $b \leq a$, then the greatest fixed point of $f$ is less than or equal to $a$.

OrderHom.isFixedPt_gfp theorem

: IsFixedPt f f.gfp

Full source

theorem isFixedPt_gfp : IsFixedPt f f.gfp :=
  f.dual.isFixedPt_lfp

Greatest Fixed Point Property: $f(\mathrm{gfp}(f)) = \mathrm{gfp}(f)$

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the greatest fixed point $\mathrm{gfp}(f)$ satisfies $f(\mathrm{gfp}(f)) = \mathrm{gfp}(f)$.

OrderHom.map_gfp theorem

: f f.gfp = f.gfp

Full source

@[simp]
theorem map_gfp : f f.gfp = f.gfp :=
  f.dual.map_lfp

Greatest Fixed Point Property: $f(\mathrm{gfp}(f)) = \mathrm{gfp}(f)$

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the greatest fixed point $\mathrm{gfp}(f)$ satisfies $f(\mathrm{gfp}(f)) = \mathrm{gfp}(f)$.

OrderHom.map_le_gfp theorem

{a : α} (ha : a ≤ f.gfp) : f a ≤ f.gfp

Full source

theorem map_le_gfp {a : α} (ha : a ≤ f.gfp) : f a ≤ f.gfp :=
  f.dual.lfp_le_map ha

Monotonicity Preserves Greatest Fixed Point Upper Bound: $a \leq \mathrm{gfp}(f) \Rightarrow f(a) \leq \mathrm{gfp}(f)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f \colon \alpha \to \alpha$, if $a \leq \mathrm{gfp}(f)$, then $f(a) \leq \mathrm{gfp}(f)$, where $\mathrm{gfp}(f)$ denotes the greatest fixed point of $f$.

OrderHom.gfp_le_map theorem

{a : α} (ha : f.gfp ≤ a) : f.gfp ≤ f a

Full source

theorem gfp_le_map {a : α} (ha : f.gfp ≤ a) : f.gfp ≤ f a :=
  f.dual.map_le_lfp ha

Monotonicity Preserves Greatest Fixed Point Bound: $\text{gfp}(f) \leq a \Rightarrow \text{gfp}(f) \leq f(a)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and a monotone function $f \colon \alpha \to \alpha$, if the greatest fixed point $\text{gfp}(f)$ of $f$ satisfies $\text{gfp}(f) \leq a$, then $\text{gfp}(f) \leq f(a)$.

OrderHom.isGreatest_gfp_le theorem

: IsGreatest {a | a ≤ f a} f.gfp

Full source

theorem isGreatest_gfp_le : IsGreatest { a | a ≤ f a } f.gfp :=
  f.dual.isLeast_lfp_le

Greatest Fixed Point is Greatest Postfixed Point

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the greatest fixed point $\mathrm{gfp}(f)$ is the greatest element of the set $\{a \in \alpha \mid a \leq f(a)\}$.

OrderHom.isGreatest_gfp theorem

: IsGreatest (fixedPoints f) f.gfp

Full source

theorem isGreatest_gfp : IsGreatest (fixedPoints f) f.gfp :=
  f.dual.isLeast_lfp

Greatest Fixed Point is Greatest Element of Fixed Points

Informal description

For a monotone function $f$ on a complete lattice $\alpha$, the greatest fixed point $\mathrm{gfp}(f)$ is the greatest element of the set of fixed points of $f$, i.e., $\mathrm{gfp}(f)$ is a fixed point of $f$ and for any other fixed point $a$ of $f$, we have $a \leq \mathrm{gfp}(f)$.

OrderHom.gfp_induction theorem

 {p : α → Prop} (step : ∀ a, p a → f.gfp ≤ a → p (f a)) (hInf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : p f.gfp

Full source

theorem gfp_induction {p : α → Prop} (step : ∀ a, p a → f.gfp ≤ a → p (f a))
    (hInf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : p f.gfp :=
  f.dual.lfp_induction step hInf

Induction Principle for Greatest Fixed Points in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ a monotone function with greatest fixed point $\mathrm{gfp}(f)$. For any predicate $p$ on $\alpha$, if: 1. For every $a \in \alpha$, if $p(a)$ holds and $\mathrm{gfp}(f) \leq a$, then $p(f(a))$ holds, and 2. For every subset $s \subseteq \alpha$, if $p(a)$ holds for all $a \in s$, then $p(\inf s)$ holds, then $p(\mathrm{gfp}(f))$ holds.

OrderHom.map_lfp_comp theorem

: f (g.comp f).lfp = (f.comp g).lfp

Full source

theorem map_lfp_comp : f (g.comp f).lfp = (f.comp g).lfp :=
  le_antisymm ((f.comp g).map_lfp ▸ f.mono (lfp_le_fixed _ <| congr_arg g (f.comp g).map_lfp)) <|
    lfp_le _ (congr_arg f (g.comp f).map_lfp).le

Fixed Point Identity: $f(\text{lfp}(g \circ f)) = \text{lfp}(f \circ g)$

Informal description

For order homomorphisms $f \colon \alpha \to_o \beta$ and $g \colon \beta \to_o \alpha$ between complete lattices, the least fixed point of $f \circ g$ satisfies $f(\text{lfp}(g \circ f)) = \text{lfp}(f \circ g)$.

OrderHom.map_gfp_comp theorem

: f (g.comp f).gfp = (f.comp g).gfp

Full source

theorem map_gfp_comp : f (g.comp f).gfp = (f.comp g).gfp :=
  f.dual.map_lfp_comp g.dual

Fixed Point Identity: $f(\mathrm{gfp}(g \circ f)) = \mathrm{gfp}(f \circ g)$

Informal description

For order homomorphisms $f \colon \alpha \to_o \beta$ and $g \colon \beta \to_o \alpha$ between complete lattices, the greatest fixed point of $f \circ g$ satisfies $f(\mathrm{gfp}(g \circ f)) = \mathrm{gfp}(f \circ g)$.

OrderHom.lfp_lfp theorem

(h : α →o α →o α) : (lfp.comp h).lfp = h.onDiag.lfp

Full source

theorem lfp_lfp (h : α →o α →o α) : (lfp.comp h).lfp = h.onDiag.lfp := by
  let a := (lfp.comp h).lfp
  refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))
  · exact lfp_le _ h.onDiag.map_lfp.le
  have ha : (lfplfp ∘ h) a = a := (lfp.comp h).map_lfp
  calc
    h a a = h a (h a).lfp := congr_arg (h a) ha.symm
    _ = (h a).lfp := (h a).map_lfp
    _ = a := ha

Least Fixed Point of Diagonal Restriction Equals Least Fixed Point of Composition with $\text{lfp}$

Informal description

For any complete lattice $\alpha$ and any monotone function $h : \alpha \to \alpha \to \alpha$, the least fixed point of the function $\text{lfp} \circ h$ is equal to the least fixed point of the diagonal restriction of $h$, i.e., $\text{lfp}(\lambda x, \text{lfp}(h(x))) = \text{lfp}(\lambda x, h(x, x))$.

OrderHom.gfp_gfp theorem

(h : α →o α →o α) : (gfp.comp h).gfp = h.onDiag.gfp

Full source

theorem gfp_gfp (h : α →o α →o α) : (gfp.comp h).gfp = h.onDiag.gfp :=
  @lfp_lfp αᵒᵈ _ <| (OrderHom.dualIso αᵒᵈ αᵒᵈ).symm.toOrderEmbedding.toOrderHom.comp h.dual

Greatest Fixed Point of Diagonal Restriction Equals Greatest Fixed Point of Composition with $\text{gfp}$

Informal description

For any complete lattice $\alpha$ and any monotone function $h : \alpha \to \alpha \to \alpha$, the greatest fixed point of the function $\text{gfp} \circ h$ is equal to the greatest fixed point of the diagonal restriction of $h$, i.e., $\text{gfp}(\lambda x, \text{gfp}(h(x))) = \text{gfp}(\lambda x, h(x, x))$.

OrderHom.gfp_const_inf_le theorem

(x : α) : (const α x ⊓ f).gfp ≤ x

Full source

theorem gfp_const_inf_le (x : α) : (constconst α x ⊓ f).gfp ≤ x :=
  (gfp_le _) fun _ hb => hb.trans inf_le_left

Greatest Fixed Point of Constrained Function is Bounded by $x$

Informal description

For any element $x$ in a complete lattice $\alpha$ and any monotone function $f : \alpha \to \alpha$, the greatest fixed point of the function $\lambda y, x \sqcap f(y)$ is less than or equal to $x$.

OrderHom.prevFixed definition

(x : α) (hx : f x ≤ x) : fixedPoints f

Full source

/-- 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`. -/
def prevFixed (x : α) (hx : f x ≤ x) : fixedPoints f :=
  ⟨(const α x ⊓ f).gfp,
    calc
      f (const α x ⊓ f).gfp = x ⊓ f (const α x ⊓ f).gfp :=
        Eq.symm <| inf_of_le_right <| (f.mono <| f.gfp_const_inf_le x).trans hx
      _ = (const α x ⊓ f).gfp := (const α x ⊓ f).map_gfp
      ⟩

Greatest fixed point below $ x $

Informal description

Given a monotone function $ f $ on a complete lattice $ \alpha $ and an element $ x \in \alpha $ such that $ f(x) \leq x $, the function `prevFixed` returns the greatest fixed point of $ f $ that is less than or equal to $ x $. This is constructed as the greatest fixed point of the function $ \lambda y, x \sqcap f(y) $.

OrderHom.nextFixed definition

(x : α) (hx : x ≤ f x) : fixedPoints f

Full source

/-- 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`. -/
def nextFixed (x : α) (hx : x ≤ f x) : fixedPoints f :=
  { f.dual.prevFixed x hx with val := (constconst α x ⊔ f).lfp }

Least fixed point above $ x $

Informal description

Given a monotone function $ f $ on a complete lattice $ \alpha $ and an element $ x \in \alpha $ such that $ x \leq f(x) $, the function `nextFixed` returns the least fixed point of $ f $ that is greater than or equal to $ x $. This is constructed as the least fixed point of the function $ \lambda y, x \sqcup f(y) $.

OrderHom.prevFixed_le theorem

{x : α} (hx : f x ≤ x) : ↑(f.prevFixed x hx) ≤ x

Full source

theorem prevFixed_le {x : α} (hx : f x ≤ x) : ↑(f.prevFixed x hx) ≤ x :=
  f.gfp_const_inf_le x

Greatest Fixed Point Below $x$ is Less Than or Equal to $x$

Informal description

For any element $x$ in a complete lattice $\alpha$ and any monotone function $f : \alpha \to \alpha$ such that $f(x) \leq x$, the greatest fixed point of $f$ below $x$ (denoted by $\mathrm{prevFixed}(f, x, hx)$) satisfies $\mathrm{prevFixed}(f, x, hx) \leq x$.

OrderHom.le_nextFixed theorem

{x : α} (hx : x ≤ f x) : x ≤ f.nextFixed x hx

Full source

theorem le_nextFixed {x : α} (hx : x ≤ f x) : x ≤ f.nextFixed x hx :=
  f.dual.prevFixed_le hx

Element is Below Its Least Fixed Point Above

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a monotone function. For any element $x \in \alpha$ such that $x \leq f(x)$, we have $x \leq \text{nextFixed}(f, x)$, where $\text{nextFixed}(f, x)$ is the least fixed point of $f$ above $x$.

OrderHom.nextFixed_le theorem

{x : α} (hx : x ≤ f x) {y : fixedPoints f} (h : x ≤ y) : f.nextFixed x hx ≤ y

Full source

theorem nextFixed_le {x : α} (hx : x ≤ f x) {y : fixedPoints f} (h : x ≤ y) :
    f.nextFixed x hx ≤ y :=
  Subtype.coe_le_coe.1 <| lfp_le _ <| sup_le h y.2.le

Least Fixed Point Above $x$ is Below Any Fixed Point Above $x$

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a monotone function. For any element $x \in \alpha$ such that $x \leq f(x)$, and any fixed point $y$ of $f$ with $x \leq y$, the least fixed point of $f$ above $x$ satisfies $\text{nextFixed}(f, x) \leq y$.

OrderHom.nextFixed_le_iff theorem

{x : α} (hx : x ≤ f x) {y : fixedPoints f} : f.nextFixed x hx ≤ y ↔ x ≤ y

Full source

@[simp]
theorem nextFixed_le_iff {x : α} (hx : x ≤ f x) {y : fixedPoints f} :
    f.nextFixed x hx ≤ y ↔ x ≤ y :=
  ⟨fun h => (f.le_nextFixed hx).trans h, f.nextFixed_le hx⟩

Characterization of Least Fixed Point Above $x$ via Inequality with Fixed Points

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a monotone function. For any element $x \in \alpha$ such that $x \leq f(x)$, and any fixed point $y$ of $f$, the least fixed point of $f$ above $x$ satisfies $\text{nextFixed}(f, x) \leq y$ if and only if $x \leq y$.

OrderHom.le_prevFixed_iff theorem

{x : α} (hx : f x ≤ x) {y : fixedPoints f} : y ≤ f.prevFixed x hx ↔ ↑y ≤ x

Full source

@[simp]
theorem le_prevFixed_iff {x : α} (hx : f x ≤ x) {y : fixedPoints f} :
    y ≤ f.prevFixed x hx ↔ ↑y ≤ x :=
  f.dual.nextFixed_le_iff hx

Characterization of Greatest Fixed Point Below $x$ via Inequality with Fixed Points

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a monotone function. For any element $x \in \alpha$ such that $f(x) \leq x$, and any fixed point $y$ of $f$, the greatest fixed point of $f$ below $x$ satisfies $y \leq \text{prevFixed}(f, x)$ if and only if $y \leq x$.

OrderHom.le_prevFixed theorem

{x : α} (hx : f x ≤ x) {y : fixedPoints f} (h : ↑y ≤ x) : y ≤ f.prevFixed x hx

Full source

theorem le_prevFixed {x : α} (hx : f x ≤ x) {y : fixedPoints f} (h : ↑y ≤ x) :
    y ≤ f.prevFixed x hx :=
  (f.le_prevFixed_iff hx).2 h

Greatest Fixed Point Below $x$ Dominates All Smaller Fixed Points

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a monotone function. For any element $x \in \alpha$ such that $f(x) \leq x$, and any fixed point $y$ of $f$ satisfying $y \leq x$, we have $y \leq \text{prevFixed}(f, x)$, where $\text{prevFixed}(f, x)$ is the greatest fixed point of $f$ below $x$.

OrderHom.le_map_sup_fixedPoints theorem

(x y : fixedPoints f) : (x ⊔ y : α) ≤ f (x ⊔ y)

Full source

theorem le_map_sup_fixedPoints (x y : fixedPoints f) : (x ⊔ y : α) ≤ f (x ⊔ y) :=
  calc
    (x ⊔ y : α) = f x ⊔ f y := congr_arg₂ (· ⊔ ·) x.2.symm y.2.symm
    _ ≤ f (x ⊔ y) := f.mono.le_map_sup x y

Supremum of Fixed Points is Below Function Value

Informal description

For any two fixed points $x$ and $y$ of a monotone function $f$ on a complete lattice, the supremum $x \sqcup y$ is less than or equal to the value of $f$ at $x \sqcup y$.

OrderHom.map_inf_fixedPoints_le theorem

(x y : fixedPoints f) : f (x ⊓ y) ≤ x.val ⊓ y.val

Full source

theorem map_inf_fixedPoints_le (x y : fixedPoints f) : f (x ⊓ y) ≤ x.val ⊓ y.val :=
  f.dual.le_map_sup_fixedPoints x y

Monotone Function Preserves Infimum of Fixed Points

Informal description

For any two fixed points $x$ and $y$ of a monotone function $f$ on a complete lattice, the value of $f$ at the infimum $x \sqcap y$ is less than or equal to the infimum of $x$ and $y$, i.e., $f(x \sqcap y) \leq x \sqcap y$.

OrderHom.le_map_sSup_subset_fixedPoints theorem

(A : Set α) (hA : A ⊆ fixedPoints f) : sSup A ≤ f (sSup A)

Full source

theorem le_map_sSup_subset_fixedPoints (A : Set α) (hA : A ⊆ fixedPoints f) :
    sSup A ≤ f (sSup A) :=
  sSup_le fun _ hx => hA hx ▸ (f.mono <| le_sSup hx)

Supremum of Fixed Points is Preserved Under Monotone Function

Informal description

For any subset $A$ of the fixed points of a monotone function $f$ on a complete lattice $\alpha$, the supremum of $A$ is less than or equal to $f$ applied to the supremum of $A$.

OrderHom.map_sInf_subset_fixedPoints_le theorem

(A : Set α) (hA : A ⊆ fixedPoints f) : f (sInf A) ≤ sInf A

Full source

theorem map_sInf_subset_fixedPoints_le (A : Set α) (hA : A ⊆ fixedPoints f) :
    f (sInf A) ≤ sInf A :=
  le_sInf fun _ hx => hA hx ▸ (f.mono <| sInf_le hx)

Monotone Function Preserves Infimum of Fixed Points

Informal description

For any subset $A$ of a complete lattice $\alpha$ consisting entirely of fixed points of a monotone function $f \colon \alpha \to \alpha$, the image of the infimum of $A$ under $f$ is less than or equal to the infimum of $A$, i.e., $f(\bigwedge A) \leq \bigwedge A$.

fixedPoints.instSemilatticeSupElemFixedPointsCoeOrderHom instance

: SemilatticeSup (fixedPoints f)

Full source

instance : SemilatticeSup (fixedPoints f) :=
  { Subtype.partialOrder _ with
    sup := fun x y => f.nextFixed (x ⊔ y) (f.le_map_sup_fixedPoints x y)
    le_sup_left := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_left.trans (f.le_nextFixed _)
    le_sup_right := fun _ _ => Subtype.coe_le_coe.1 <| le_sup_right.trans (f.le_nextFixed _)
    sup_le := fun _ _ _ hxz hyz => f.nextFixed_le _ <| sup_le hxz hyz }

Join-Semilattice Structure on Fixed Points of a Monotone Function

Informal description

The set of fixed points of a monotone function $f$ on a complete lattice forms a join-semilattice, where the supremum operation is inherited from the underlying lattice.

fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHom instance

: SemilatticeInf (fixedPoints f)

Full source

instance : SemilatticeInf (fixedPoints f) :=
  { OrderDual.instSemilatticeInf (fixedPoints f.dual) with
    inf := fun x y => f.prevFixed (x ⊓ y) (f.map_inf_fixedPoints_le x y) }

Meet-Semilattice Structure on Fixed Points of a Monotone Function

Informal description

The set of fixed points of a monotone function $f$ on a complete lattice forms a meet-semilattice, where the infimum operation is inherited from the underlying lattice.

fixedPoints.instCompleteSemilatticeSupElemFixedPointsCoeOrderHom instance

: CompleteSemilatticeSup (fixedPoints f)

Full source

instance : CompleteSemilatticeSup (fixedPoints f) :=
  { Subtype.partialOrder _ with
    sSup := fun s =>
      f.nextFixed (sSup (Subtype.valSubtype.val '' s))
        (f.le_map_sSup_subset_fixedPoints (Subtype.valSubtype.val '' s)
          fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
    le_sSup := fun _ _ hx =>
      Subtype.coe_le_coe.1 <| le_trans (le_sSup <| Set.mem_image_of_mem _ hx) (f.le_nextFixed _)
    sSup_le := fun _ _ hx => f.nextFixed_le _ <| sSup_le <| Set.forall_mem_image.2 hx }

Complete Join-Semilattice Structure on Fixed Points

Informal description

For any monotone function $f$ on a complete lattice $\alpha$, the set of fixed points of $f$ forms a complete join-semilattice. That is, every nonempty subset of fixed points has a least upper bound within the set of fixed points.

fixedPoints.instCompleteSemilatticeInfElemFixedPointsCoeOrderHom instance

: CompleteSemilatticeInf (fixedPoints f)

Full source

instance : CompleteSemilatticeInf (fixedPoints f) :=
  { Subtype.partialOrder _ with
    sInf := fun s =>
      f.prevFixed (sInf (Subtype.valSubtype.val '' s))
        (f.map_sInf_subset_fixedPoints_le (Subtype.valSubtype.val '' s) fun _ ⟨x, hx⟩ => hx.2 ▸ x.2)
    le_sInf := fun _ _ hx => f.le_prevFixed _ <| le_sInf <| Set.forall_mem_image.2 hx
    sInf_le := fun _ _ hx =>
      Subtype.coe_le_coe.1 <| le_trans (f.prevFixed_le _) (sInf_le <| Set.mem_image_of_mem _ hx) }

Complete Meet-Semilattice Structure on Fixed Points

Informal description

For any monotone function $f$ on a complete lattice $\alpha$, the set of fixed points of $f$ forms a complete meet-semilattice. That is, every nonempty subset of fixed points has a greatest lower bound within the set of fixed points.

fixedPoints.completeLattice instance

: CompleteLattice (fixedPoints f)

Full source

/-- **Knaster-Tarski Theorem**: The fixed points of `f` form a complete lattice. -/
instance completeLattice : CompleteLattice (fixedPoints f) where
  __ := inferInstanceAs (SemilatticeInf (fixedPoints f))
  __ := inferInstanceAs (SemilatticeSup (fixedPoints f))
  __ := inferInstanceAs (CompleteSemilatticeInf (fixedPoints f))
  __ := inferInstanceAs (CompleteSemilatticeSup (fixedPoints f))
  top := ⟨f.gfp, f.isFixedPt_gfp⟩
  bot := ⟨f.lfp, f.isFixedPt_lfp⟩
  le_top x := f.le_gfp x.2.ge
  bot_le x := f.lfp_le x.2.le

Knaster-Tarski Theorem: Fixed Points Form a Complete Lattice

Informal description

For any monotone function $f$ on a complete lattice $\alpha$, the set of fixed points of $f$ forms a complete lattice. This means that every subset of fixed points has both a supremum and an infimum within the set of fixed points.

fixedPoints.lfp_eq_sSup_iterate theorem

(h : ωScottContinuous f) : f.lfp = ⨆ n, f^[n] ⊥

Full source

/-- **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 lfp_eq_sSup_iterate (h : ωScottContinuous f) :
    f.lfp = ⨆ n, f^[n] ⊥ := by
  apply le_antisymm
  · apply lfp_le_fixed
    exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)
  · apply le_lfp
    intro a h_a
    exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Kleene's Fixed Point Theorem: $\text{lfp}(f) = \bigsqcup_n f^n(\bot)$ for $\omega$-Scott continuous $f$

Informal description

Let $f$ be a monotone function on a complete lattice $\alpha$ that is $\omega$-Scott continuous. Then the least fixed point of $f$ is equal to the supremum of the iterates of $f$ applied to the bottom element $\bot$: \[ \text{lfp}(f) = \bigsqcup_{n \in \mathbb{N}} f^n(\bot) \] where $f^n$ denotes the $n$-th iterate of $f$.

fixedPoints.gfp_eq_sInf_iterate theorem

(h : ωScottContinuous f.dual) : f.gfp = ⨅ n, f^[n] ⊤

Full source

theorem gfp_eq_sInf_iterate (h : ωScottContinuous f.dual) :
    f.gfp = ⨅ n, f^[n] ⊤ :=
  lfp_eq_sSup_iterate f.dual h

Greatest Fixed Point as Infimum of Iterates: $\text{gfp}(f) = \bigsqcap_n f^n(\top)$ for $\omega$-Scott continuous dual

Informal description

Let $f$ be a monotone function on a complete lattice $\alpha$ such that its dual function is $\omega$-Scott continuous. Then the greatest fixed point of $f$ is equal to the infimum of the iterates of $f$ applied to the top element $\top$: \[ \text{gfp}(f) = \bigsqcap_{n \in \mathbb{N}} f^n(\top) \] where $f^n$ denotes the $n$-th iterate of $f$.

Mathlib.Order.FixedPoints

Main definitions

Tags