X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Finfsup.ma;h=b3babd1b5f43f3e0b5162855ac47fd3f400b4e7f;hb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;hp=05b497cc51c7ac924ae3a5c0f7b61f1b46901608;hpb=ea7c93bf4177982ff09d429a3a818e8b5f937ea1;p=helm.git

diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index 05b497cc5..b3babd1b5 100644
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -25,8 +25,8 @@ definition infimum ≝
     
 (* 3.20 *)
 lemma supremum_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → (* BUG again the wrong coercion is chosen *)
-   ∀x,y:apart_of_metric_space ? ml.supremum ?? xn x → supremum ?? xn y → x ≈ y.
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → 
+   ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
 intros (R ml xn Hxn x y Sx Sy);
 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
 apply (tends_uniq ?? xn ?? Hx Hy);
@@ -42,6 +42,18 @@ definition ank ≝
       [ O ⇒ (shift ?? xn k) O
       | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
     in ank_aux.
+     
+notation < "'a'\sup k" non associative with precedence 50 for
+ @{ 'ank $x $k }.
+ 
+interpretation "ank" 'ank x k =
+ (cic:/matita/infsup/ank.con _ _ x k).      
+
+notation < "'a'(k \atop n)" non associative with precedence 50 for
+ @{ 'ank2 $x $k $n }.
+ 
+interpretation "ank2" 'ank2 x k n =
+ (cic:/matita/infsup/ank.con _ _ x k n).      
     
 definition bnk ≝
   λR.λml:mlattice R.λxn:sequence ml.λk:nat.
@@ -50,16 +62,28 @@ definition bnk ≝
       [ O ⇒ (shift ?? xn k) O
       | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
     in bnk_aux.
+
+notation < "'b'\sup k" non associative with precedence 50 for
+ @{ 'bnk $x $k }.
+ 
+interpretation "bnk" 'bnk x k =
+ (cic:/matita/infsup/bnk.con _ _ x k).      
+
+notation < "('b' \sup k) \sub n" non associative with precedence 50 for
+ @{ 'bnk2 $x $k $n }.
+ 
+interpretation "bnk2" 'bnk2 x k n =
+ (cic:/matita/infsup/bnk.con _ _ x k n).      
     
 lemma ank_decreasing: 
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀m.decreasing ? (ank ?? xn m).
-intros (R ml xn m); unfold; intro n; simplify; apply lem;
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
+intros (R ml xn k); unfold; intro n; simplify; apply lem;
 qed.
 
 (* 3.26 *)
 lemma ankS:
   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
-    ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
+   ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
 intros (R ml xn k n); elim n; simplify; [apply meet_comm]  
 simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
 apply (Eq≈ ? (meet_assoc ????));    
@@ -68,6 +92,110 @@ apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
 apply meet_comm;
 qed.    
-   
-   
-   
\ No newline at end of file
+
+lemma bnkS:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
+   ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
+intros (R ml xn k n); elim n; simplify; [apply join_comm]  
+simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
+apply (Eq≈ ? (join_assoc ????));    
+apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
+apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+apply join_comm;
+qed.    
+
+lemma le_asnk_ansk:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
+   (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
+intros (R ml xn k n);
+apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
+qed.   
+
+lemma le_bnsk_bsnk:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
+   (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
+intros (R ml xn k n);
+apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????)); 
+apply (Le≫ ? (join_comm ???));
+apply lej;
+qed.   
+
+
+(* 3.27 *)
+lemma inf_increasing:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.
+   ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → 
+     increasing ml alpha.
+intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold; 
+intro r; 
+elim (H r) (H1r H2r);
+elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
+intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
+lapply (H1r (S w)) as Hsw; clear H1r;
+lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
+cases (H Hw);
+qed.
+
+lemma sup_decreasing:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.
+   ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) → 
+     decreasing ml alpha.
+intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; 
+intro r; 
+elim (H r) (H1r H2r);
+elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
+intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
+lapply (H1r (S w)) as Hsw; clear H1r;
+lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
+cases (H Hw);
+qed.
+
+(* 3.28 *)
+definition liminf ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+    ∃alpha:sequence ml. 
+      (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
+  
+definition limsup ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+    ∃alpha:sequence ml. 
+      (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
+  
+(* 3.29 *)  
+alias symbol "and" = "constructive and".
+definition lim ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+   (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
+  
+(* 3.30 *)   
+lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
+   lim ?? xn x → xn ⇝ x.
+intros (R ml xn x Hl); 
+unfold in Hl; unfold limsup in Hl; unfold liminf in Hl; 
+(* decompose; *)
+elim Hl (low Hl_); clear Hl;   
+elim Hl_ (up Hl); clear Hl_;  
+elim Hl (Hl_ E1); clear Hl;   
+elim Hl_ (Hl E2); clear Hl_;  
+elim Hl (H1 H2); clear Hl;   
+elim H1 (alpha Halpha); clear H1;   
+elim H2 (beta Hbeta); clear H2;
+apply (sandwich ?? alpha beta); 
+[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
+    lapply (sup_increasing ????? Ha6) as Ha7;
+
+    unfold strong_sup in Halpha Hbeta;
+    unfold strong_inf in Halpha Hbeta;
+    unfold lower_bound in Halpha Hbeta;
+    unfold upper_bound in Halpha Hbeta; 
+    elim (Halpha m) (Ha5 Ha6); clear Halpha;
+    elim Ha5 (Ha1 Ha2); clear Ha5;
+    elim Ha6 (Ha3 Ha4); clear Ha6;
+    split; 
+    [1: intro H; elim (Ha2 ? H) (w H1);
+        elim (Ha4 ? H1);
+    
+    
+    
+  
\ No newline at end of file