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 (* NOT DUALIZED *)
  20 alias symbol "low" = "lower".
  21 alias id "le" = "cic:/matita/dama/ordered_set/le.con".
  22 lemma order_converges_bigger_lowsegment:
  23   ∀C:ordered_set.
  24    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
  25      ∀x:C.∀p:order_converge C a x.
  26        ∀j. seg_l (os_l C) s (λl.le (os_l C) l (pi1exT23 ???? p j)).
  27 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
  28 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
  29 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
  30 cases (wloss_prop (os_l C))(W W);rewrite <W;
  31 [ intro H2; cases (SSa (seg_l_ C s) H2) (w Hw); simplify in Hw;
  32   lapply (H (w+j)) as K; unfold in K;
  33   whd in K:(? % ? ? ? ?); simplify in K:(%); rewrite <W in K; cases K;
  34   whd in H1:(? % ? ? ? ?); simplify in H1:(%); rewrite <W in H1;
  35   simplify in H1; apply (H1 Hw);
  36 | intro H2; cases (SSa (seg_u_ C s) H2) (w Hw); simplify in Hw;
  37   lapply (H (w+j)) as K; unfold in K;
  38   whd in K:(? % ? ? ? ?);simplify in K:(%); rewrite <W in K; cases K;
  39   whd in H3:(? % ? ? ? ?);simplify in H3:(%); rewrite <W in H3;
  40   simplify in H3; apply (H3 Hw);]
  41 qed.
  42
  43 lemma order_converges_smaller_upsegment:
  44   ∀C:ordered_set.
  45    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
  46      ∀x:C.∀p:order_converge C a x.
  47        ∀j. seg_u (os_l C) s (λu.le (os_l C) (pi2exT23 ???? p j) u).
  48 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
  49 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
  50 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
  51 cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite <W;
  52 [ intro H2; cases (SIa (seg_u_ (os_l C) s) H2) (w Hw); simplify in Hw;
  53   lapply (H (w+j)) as K; unfold in K; whd in K:(? % ? ? ? ?); simplify in K:(%);
  54   rewrite <W in K; cases K; whd in H3:(? % ? ? ? ?); simplify in H3:(%); rewrite <W in H3;
  55   simplify in H3; apply (H3 Hw);
  56 | intro H2; cases (SIa (seg_l_ C s) H2) (w Hw); simplify in Hw;
  57   lapply (H (w+j)) as K; unfold in K;  whd in K:(? % ? ? ? ?); simplify in K:(%);
  58   rewrite <W in K; cases K; whd in H1:(? % ? ? ? ?); simplify in H1:(%);
  59   rewrite <W in H1; simplify in H1; apply (H1 Hw);]
  60 qed.
  61
  62 alias symbol "upp" = "uppper".
  63 alias symbol "leq" = "Ordered set less or equal than".
  64 lemma cases_in_segment:
  65   ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → seg_l C s (λl.l ≤≤ x) ∧ seg_u C s (λu.x ≤≤ u).
  66 intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
  67 cases H; split; assumption;
  68 qed.
  69
  70 lemma trans_under_upp:
  71  ∀O:ordered_set.∀s:‡O.∀x,y:O.
  72   x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).
  73 intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
  74 apply (le_transitive ??? H H1);
  75 qed.
  76
  77 lemma trans_under_low:
  78  ∀O:ordered_set.∀s:‡O.∀x,y:O.
  79   y ≤ x → 𝕝_s (λl.l ≤ y) → 𝕝_s (λl.l ≤ x).
  80 intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
  81 apply (le_transitive ??? H1 H);
  82 qed.
  83
  84 lemma l2sl:
  85   ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
  86 intros; unfold in H ⊢ %; intro; apply H; clear H; unfold in H1 ⊢ %;
  87 cases (wloss_prop C) (W W); whd in H1:(? (% ? ?) ? ? ? ?); simplify in H1:(%);
  88 rewrite < W in H1 ⊢ %; apply H1;
  89 qed.
  90
  91 (* Theorem 3.10 *)
  92 theorem lebesgue_oc:
  93   ∀C:ordered_uniform_space.
  94    (∀s:‡C.order_continuity {[s]}) →
  95     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
  96      ∀x:C.a order_converges x →
  97       x ∈ s ∧
  98       ∀h:x ∈ s.
  99        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
 100 intros;
 101 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
 102 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 103 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 104 cut (∀i.xi i ∈ s) as Hxi; [2:
 105   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
 106   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 107   apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
 108 cut (∀i.yi i ∈ s) as Hyi; [2:
 109   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
 110   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 111   apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
 112 split;
 113 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
 114 |2: intros 3 (h);
 115     letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 116     letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 117     letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 118     apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
 119     [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
 120         [apply (l2sl ? s (Xi j) (Ai j) (H5 0));|apply (l2sl ? s (Ai j) (Yi j) (H7 0))]
 121     |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl ? s (Xi i) (Xi (S i)) (H3 i));]
 122         cases H4; split; [intro i; apply (l2sl ? s (Xi i) ≪x,h≫ (H5 i))]
 123         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s ? y Hy)]
 124         exists [apply w] apply (x2sx ? s (Xi w) y H7);
 125     |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl ? s (Yi (S i))  (Yi i) (H3 i));]
 126         cases H4; split; [intro i; apply (l2sl ? s ≪x,h≫ (Yi i) (H5 i))]
 127         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s y ≪x,h≫ Hy)]
 128         exists [apply w] apply (x2sx ? s y (Yi w) H7);]]
 129 qed.
 130
 131
 132 (* Theorem 3.9 *)
 133 theorem lebesgue_se:
 134   ∀C:ordered_uniform_space.property_sigma C →
 135    (∀s:‡C.exhaustive {[s]}) →
 136     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
 137      ∀x:C.a order_converges x →
 138       x ∈ s ∧
 139       ∀h:x ∈ s.
 140        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
 141 intros (C S);
 142 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
 143 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 144 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 145 cut (∀i.xi i ∈ s) as Hxi; [2:
 146   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
 147   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 148   apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
 149 cut (∀i.yi i ∈ s) as Hyi; [2:
 150   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
 151   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 152   apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
 153 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 154 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 155 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
 156 cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
 157 split; [1: assumption]
 158 intros 3;
 159 lapply (uparrow_upperlocated  xi x Hx)as Ux;
 160 lapply (downarrow_lowerlocated  yi x Hy)as Uy;
 161 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 162 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
 163 intro j; cases (Hxy j); cases H7; cases H8; split;
 164 [apply (l2sl ? s (Xi j) (Ai j) (H9 0));|apply (l2sl ? s (Ai j) (Yi j) (H11 0))]
 165 qed.
 166
 167
 168