blob: 58d768c0e6142394cbac792b17145fcddc7e7311 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
import Mathlib
variable {α : Type} [CompleteLattice α]
structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where
fixedPt : Function.IsFixedPt f x
least : ∀ y, Function.IsFixedPt f y → x ≤ y
structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where
fixedPt : Function.IsFixedPt f x
greatest : ∀ y, Function.IsFixedPt f y → y ≤ x
namespace FixedPoints
def lfp (f : α → α) : α := sInf { x | f x ≤ x }
def gfp (f : α → α) : α := sSup { x | x ≤ f x }
lemma lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where
fixedPt := by
have hmem : f (lfp f) ≤ lfp f := by
rw [lfp, le_sInf_iff]
intro x hx
grw [hf (sInf_le hx)]
exact hx
apply Std.IsPartialOrder.le_antisymm
· exact hmem
· exact (sInf_le (hf hmem))
least := by
intro x hfix
apply sInf_le
simp [show f x = x from hfix]
-- TODO: Avoid repitition
lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where
fixedPt := by
have hmem : gfp f ≤ f (gfp f) := by
rw [gfp, sSup_le_iff]
intro x hx
grw [show x ≤ f x from hx]
exact hf (le_sSup hx)
apply Std.IsPartialOrder.le_antisymm
· apply le_sSup
exact hf hmem
· exact hmem
greatest := by
intro x hfix
apply le_sSup
simp [show f x = x from hfix]
end FixedPoints
|
