lebesgue proved

[helm.git] / helm / software / matita / contribs / dama / dama / lebesgue.ma

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 85f686da3ebed0968b3e7970ee599d3fb552b9a5..bab1e26faef33c6bc09544c31b7895ae2fd1b8cf 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -16,10 +16,30 @@
 include "sandwich.ma".
 include "property_exhaustivity.ma".
 
-le x_i e y_i stanno o no nel segmento?
+lemma order_converges_bigger_lowsegment:
+  ∀C:ordered_set.
+   ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.∀p:a order_converges x. 
+       ∀j.l ≤ (fst p) j.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H8 ? H2);
+cases (H (w1+j)); apply (H12 H7);
+qed.   
 
+lemma order_converges_smaller_upsegment:
+  ∀C:ordered_set.
+   ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.∀p:a order_converges x. 
+       ∀j.(snd p) j ≤ u.
+intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
+intro H2; cases (H10 ? H2);
+cases (H (w1+j)); apply (H11 H7);
+qed.   
+     
 (* Theorem 3.10 *)
-theorem lebesgue:
+theorem lebesgue_oc:
   ∀C:ordered_uniform_space.
    (∀l,u:C.order_continuity {[l,u]}) →
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
@@ -31,14 +51,41 @@ theorem lebesgue:
          (segment_ordered_uniform_space C l u))
         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
         (sig_in ?? x h).
-intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; 
-cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
+intros;
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+  intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+  apply (le_transitive ???? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+  intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+  apply (le_transitive ????? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H2;
 split;
-[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
-
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+    [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+    |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3 (h);
+    letin X ≝ (sig_in ?? x h);
+    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+        [apply (H5 0);|apply (H7 0)]
+    |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        exists [apply w] apply H7; 
+    |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        exists [apply w] apply H7;]]
+qed.
+ 
 
 (* Theorem 3.9 *)
-theorem lebesgue:
+theorem lebesgue_se:
   ∀C:ordered_uniform_space.property_sigma C →
    (∀l,u:C.exhaustive {[l,u]}) →
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
@@ -50,22 +97,34 @@ theorem lebesgue:
          (segment_ordered_uniform_space C l u))
         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
         (sig_in ?? x h). 
-intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8; 
-cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
-lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
-lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
-cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x); 
-[ split; assumption]
-split; simplify;
- [1: intro;  cases (H7 n); cases H3;
- 
- 
- lapply (sandwich ? x xi yi a );
-  [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
-  |3: intros 2;  
-      cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x); 
-      [1: 
-
-lapply (restrict_uniform_convergence ? H ?? (H1 l u) 
-         (λn:nat.sig_in ?? (a n) (H2 n)) x);
-  [2:split; assumption]
\ No newline at end of file
+intros (C S);
+generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
+generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
+cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
+cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
+  intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
+  apply (le_transitive ???? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H3;
+cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
+  intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
+  apply (le_transitive ????? (H7 0)); simplify; 
+  cases (H1 i); assumption;] clear H2;
+split;
+[1: cases Hx; cases H3; cases Hy; cases H7; split;
+    [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
+    |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
+|2: intros 3;
+    lapply (uparrow_upperlocated ? xi x Hx)as Ux;
+    lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
+    letin X ≝ (sig_in ?? x h);
+    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
+    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
+    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
+    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    [1: intro j; cases (Hxy j); cases H3; cases H4; split;
+        [apply (H5 0);|apply (H7 0)]
+    |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
+        apply (H4 h);
+    |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
+        apply (H4 h);]]
+qed.