1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sandwich_corollary.ma".
19 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
20 increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
23 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
24 decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
28 ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn →
29 ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
30 intros (R ml xn Hxn x y Sx Sy);
31 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
32 apply (tends_uniq ?? xn ?? Hx Hy);
35 definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
36 λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
39 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
40 let rec ank_aux (i : nat) ≝
42 [ O ⇒ (shift ?? xn k) O
43 | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
46 notation < "'a'\sup k" non associative with precedence 50 for
49 interpretation "ank" 'ank x k =
50 (cic:/matita/infsup/ank.con _ _ x k).
52 notation < "'a'(k \atop n)" non associative with precedence 50 for
55 interpretation "ank2" 'ank2 x k n =
56 (cic:/matita/infsup/ank.con _ _ x k n).
59 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
60 let rec bnk_aux (i : nat) ≝
62 [ O ⇒ (shift ?? xn k) O
63 | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
66 notation < "'b'\sup k" non associative with precedence 50 for
69 interpretation "bnk" 'bnk x k =
70 (cic:/matita/infsup/bnk.con _ _ x k).
72 notation < "('b' \sup k) \sub n" non associative with precedence 50 for
75 interpretation "bnk2" 'bnk2 x k n =
76 (cic:/matita/infsup/bnk.con _ _ x k n).
79 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
80 intros (R ml xn k); unfold; intro n; simplify; apply lem;
85 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
86 ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
87 intros (R ml xn k n); elim n; simplify; [apply meet_comm]
88 simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
89 apply (Eq≈ ? (meet_assoc ????));
90 apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
91 apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
92 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
97 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
98 ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
99 intros (R ml xn k n); elim n; simplify; [apply join_comm]
100 simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
101 apply (Eq≈ ? (join_assoc ????));
102 apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
103 apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
104 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
109 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
110 (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
111 intros (R ml xn k n);
112 apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
116 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
117 (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
118 intros (R ml xn k n);
119 apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????));
120 apply (Le≫ ? (join_comm ???));
126 lemma inf_increasing:
127 ∀R.∀ml:mlattice R.∀xn:sequence ml.
128 ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) →
130 intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold;
132 elim (H r) (H1r H2r);
133 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
134 intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
135 lapply (H1r (S w)) as Hsw; clear H1r;
136 lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
140 lemma sup_decreasing:
141 ∀R.∀ml:mlattice R.∀xn:sequence ml.
142 ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) →
144 intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
146 elim (H r) (H1r H2r);
147 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
148 intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
149 lapply (H1r (S w)) as Hsw; clear H1r;
150 lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
156 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
158 (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
161 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
163 (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
166 alias symbol "and" = "constructive and".
168 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
169 (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
172 lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
173 lim ?? xn x → xn ⇝ x.
174 intros (R ml xn x Hl);
175 unfold in Hl; unfold limsup in Hl; unfold liminf in Hl;
177 elim Hl (low Hl_); clear Hl;
178 elim Hl_ (up Hl); clear Hl_;
179 elim Hl (Hl_ E1); clear Hl;
180 elim Hl_ (Hl E2); clear Hl_;
181 elim Hl (H1 H2); clear Hl;
182 elim H1 (alpha Halpha); clear H1;
183 elim H2 (beta Hbeta); clear H2;
184 apply (sandwich ?? alpha beta);
185 [1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
186 lapply (sup_increasing ????? Ha6) as Ha7;
188 unfold strong_sup in Halpha Hbeta;
189 unfold strong_inf in Halpha Hbeta;
190 unfold lower_bound in Halpha Hbeta;
191 unfold upper_bound in Halpha Hbeta;
192 elim (Halpha m) (Ha5 Ha6); clear Halpha;
193 elim Ha5 (Ha1 Ha2); clear Ha5;
194 elim Ha6 (Ha3 Ha4); clear Ha6;
196 [1: intro H; elim (Ha2 ? H) (w H1);