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 lemma trans_under_upp:
  63  ∀O:ordered_set.∀s:‡O.∀x,y:O.
  64   x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).
  65 intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
  66 apply (le_transitive ??? H H1);
  67 qed.
  68
  69 lemma trans_under_low:
  70  ∀O:ordered_set.∀s:‡O.∀x,y:O.
  71   y ≤ x → 𝕝_s (λl.l ≤ y) → 𝕝_s (λl.l ≤ x).
  72 intros; cases (wloss_prop (os_l O)) (W W); unfold; unfold in H1; rewrite<W in H1 ⊢ %;
  73 apply (le_transitive ??? H1 H);
  74 qed.
  75
  76 lemma l2sl:
  77   ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
  78 intros; unfold in H ⊢ %; intro; apply H; clear H; unfold in H1 ⊢ %;
  79 cases (wloss_prop C) (W W); whd in H1:(? (% ? ?) ? ? ? ?); simplify in H1:(%);
  80 rewrite < W in H1 ⊢ %; apply H1;
  81 qed.
  82
  83 (* Theorem 3.10 *)
  84 theorem lebesgue_oc:
  85   ∀C:ordered_uniform_space.
  86    (∀s:‡C.order_continuity {[s]}) →
  87     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
  88      ∀x:C.a order_converges x →
  89       x ∈ s ∧
  90       ∀h:x ∈ s.
  91        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
  92 intros;
  93 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
  94 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
  95 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
  96 cut (∀i.xi i ∈ s) as Hxi; [2:
  97   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
  98   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
  99   apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
 100 cut (∀i.yi i ∈ s) as Hyi; [2:
 101   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
 102   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 103   apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
 104 split;
 105 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
 106 |2: intros 3 (h);
 107     letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 108     letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 109     letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 110     apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
 111     [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
 112         [apply (l2sl ? s (Xi j) (Ai j) (H5 0));|apply (l2sl ? s (Ai j) (Yi j) (H7 0))]
 113     |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));]
 114         cases H4; split; [intro i; apply (l2sl ? s (Xi i) ≪x,h≫ (H5 i))]
 115         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s ? y Hy)]
 116         exists [apply w] apply (x2sx ? s (Xi w) y H7);
 117     |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));]
 118         cases H4; split; [intro i; apply (l2sl ? s ≪x,h≫ (Yi i) (H5 i))]
 119         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s y ≪x,h≫ Hy)]
 120         exists [apply w] apply (x2sx ? s y (Yi w) H7);]]
 121 qed.
 122
 123
 124 (* Theorem 3.9 *)
 125 theorem lebesgue_se:
 126   ∀C:ordered_uniform_space.property_sigma C →
 127    (∀s:‡C.exhaustive {[s]}) →
 128     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
 129      ∀x:C.a order_converges x →
 130       x ∈ s ∧
 131       ∀h:x ∈ s.
 132        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
 133 intros (C S);
 134 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
 135 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 136 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 137 cut (∀i.xi i ∈ s) as Hxi; [2:
 138   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
 139   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 140   apply (trans_under_upp ?? (xi i) (a i) K Pu);] clear H3;
 141 cut (∀i.yi i ∈ s) as Hyi; [2:
 142   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
 143   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 144   apply (trans_under_low ?? (yi i) (a i) K Pl);] clear H2;
 145 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 146 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 147 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
 148 cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
 149 split; [1: assumption]
 150 intros 3;
 151 lapply (uparrow_upperlocated  xi x Hx)as Ux;
 152 lapply (downarrow_lowerlocated  yi x Hy)as Uy;
 153 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 154 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
 155 intro j; cases (Hxy j); cases H7; cases H8; split;
 156 [apply (l2sl ? s (Xi j) (Ai j) (H9 0));|apply (l2sl ? s (Ai j) (Yi j) (H11 0))]
 157 qed.
 158
 159
 160