From 3cd093c8c3f5454514802e5d3ae5edc150dbbf72 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 9 Jun 2008 14:11:17 +0000
Subject: [PATCH] initial work on lebesque

---
 .../matita/contribs/dama/dama/depends         | 19 ++---
 .../matita/contribs/dama/dama/lebesgue.ma     | 71 +++++++++++++++++++
 .../matita/contribs/dama/dama/supremum.ma     |  2 +-
 3 files changed, 82 insertions(+), 10 deletions(-)
 create mode 100644 helm/software/matita/contribs/dama/dama/lebesgue.ma

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 128afd683..aa4bd85f9 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,16 +1,17 @@
-sandwich.ma ordered_uniform.ma
-property_sigma.ma ordered_uniform.ma
-uniform.ma supremum.ma
 bishop_set.ma ordered_set.ma
+extra.ma bishop_set_rewrite.ma
+ordered_set.ma cprop_connectives.ma
+cprop_connectives.ma logic/equality.ma
+bishop_set_rewrite.ma bishop_set.ma
 sequence.ma nat/nat.ma
-ordered_uniform.ma uniform.ma
+uniform.ma supremum.ma
 supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
-property_exhaustivity.ma ordered_uniform.ma
-bishop_set_rewrite.ma bishop_set.ma
-cprop_connectives.ma logic/equality.ma
 nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
-ordered_set.ma cprop_connectives.ma
-extra.ma bishop_set_rewrite.ma
+property_sigma.ma ordered_uniform.ma
+ordered_uniform.ma uniform.ma
+property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
+lebesgue.ma property_exhaustivity.ma sandwich.ma
+sandwich.ma ordered_uniform.ma
 logic/equality.ma 
 nat/compare.ma 
 nat/nat.ma 
diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
new file mode 100644
index 000000000..85f686da3
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* manca un pezzo del pullback, se inverto poi non tipa *)
+include "sandwich.ma".
+include "property_exhaustivity.ma".
+
+le x_i e y_i stanno o no nel segmento?
+
+(* Theorem 3.10 *)
+theorem lebesgue:
+  ∀C:ordered_uniform_space.
+   (∀l,u:C.order_continuity {[l,u]}) →
+    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.a order_converges x → 
+      x ∈ [l,u] ∧ 
+      ∀h:x ∈ [l,u]. (* manca il pullback? *)
+       uniform_converge 
+        (uniform_space_OF_ordered_uniform_space 
+         (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;
+split;
+[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
+
+
+(* Theorem 3.9 *)
+theorem lebesgue:
+  ∀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]. 
+     ∀x:C.a order_converges x → 
+      x ∈ [l,u] ∧ 
+      ∀h:x ∈ [l,u]. (* manca il pullback? *)
+       uniform_converge 
+        (uniform_space_OF_ordered_uniform_space 
+         (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
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index b99323140..a3aa83d6a 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -178,7 +178,7 @@ alias symbol "and" = "constructive and".
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    ∃l:sequence O.∃u:sequence O.
-    l is_increasing ∧ u is_decreasing ∧ l ↑ x ∧ u ↓ x ∧
+    (*l is_increasing ∧ u is_decreasing ∧*) l ↑ x ∧ u ↓ x ∧
     ∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i)).
     
 notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
-- 
2.39.2