]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/dama/dama/lebesgue.ma
e1fbd0a5a75cac9f840d207833e3319214680224
[helm.git] / helm / software / matita / contribs / dama / dama / lebesgue.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* manca un pezzo del pullback, se inverto poi non tipa *)
16 include "sandwich.ma".
17 include "property_exhaustivity.ma".
18
19 lemma order_converges_bigger_lowsegment:
20   ∀C:ordered_set.
21    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
22      ∀x:C.∀p:a order_converges x. 
23        ∀j.l ≤ (pi1exT23 ???? p) j.
24 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
25 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
26 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
27 intro H2; cases (SSa ? H2) (w Hw); simplify in Hw;
28 cases (H (w+j)) (Hal Hau); apply (Hau Hw);
29 qed.   
30
31 lemma order_converges_smaller_upsegment:
32   ∀C:ordered_set.
33    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
34      ∀x:C.∀p:a order_converges x. 
35        ∀j.(pi2exT23 ???? p) j ≤ u.
36 intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
37 cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
38 intro H2; cases (H10 ? H2);
39 cases (H (w1+j)); apply (H11 H7);
40 qed.   
41      
42 (* Theorem 3.10 *)
43 theorem lebesgue_oc:
44   ∀C:ordered_uniform_space.
45    (∀l,u:C.order_continuity {[l,u]}) →
46     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
47      ∀x:C.a order_converges x → 
48       x ∈ [l,u] ∧ 
49       ∀h:x ∈ [l,u].
50        uniform_converge {[l,u]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
51 intros;
52 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
53 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
54 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
55 cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
56   intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
57   apply (le_transitive ???? (H7 0)); simplify; 
58   cases (H1 i); assumption;] clear H3;
59 cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
60   intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
61   apply (le_transitive ????? (H7 0)); simplify; 
62   cases (H1 i); assumption;] clear H2;
63 split;
64 [1: cases Hx; cases H3; cases Hy; cases H7; split;
65     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
66     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
67 |2: intros 3 (h);
68     letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
69     letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
70     letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
71     apply (sandwich {[l,u]} ≪?,h≫ Xi Yi Ai); try assumption;
72     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
73         [apply (H5 0);|apply (H7 0)]
74     |2: cases (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
75         cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
76         exists [apply w] apply H7; 
77     |3: cases (H l u Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
78         cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
79         exists [apply w] apply H7;]]
80 qed.
81  
82
83 (* Theorem 3.9 *)
84 theorem lebesgue_se:
85   ∀C:ordered_uniform_space.property_sigma C →
86    (∀l,u:C.exhaustive {[l,u]}) →
87     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
88      ∀x:C.a order_converges x → 
89       x ∈ [l,u] ∧ 
90       ∀h:x ∈ [l,u].
91        uniform_converge {[l,u]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
92 intros (C S);
93 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
94 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
95 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
96 cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
97   intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
98   apply (le_transitive ???? (H7 0)); simplify; 
99   cases (H1 i); assumption;] clear H3;
100 cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
101   intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
102   apply (le_transitive ????? (H7 0)); simplify; 
103   cases (H1 i); assumption;] clear H2;
104 split;
105 [1: cases Hx; cases H3; cases Hy; cases H7; split;
106     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
107     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
108 |2: intros 3;
109     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
110     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
111     letin Xi ≝ (⌊n,≪xi n,Hxi n≫⌋);
112     letin Yi ≝ (⌊n,≪yi n,Hyi n≫⌋);
113     letin Ai ≝ (⌊n,≪a n,H1 n≫⌋);
114     apply (sandwich {[l,u]} ≪x,h≫ Xi Yi Ai); try assumption;
115     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
116         [apply (H5 0);|apply (H7 0)]
117     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
118         apply (H4 h);
119     |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
120         apply (H4 h);]]
121 qed.