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 ≤ (fst 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.(snd 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]. (* manca il pullback? *)
  50        uniform_converge
  51         (uniform_space_OF_ordered_uniform_space
  52          (segment_ordered_uniform_space C l u))
  53         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
  54         (sig_in ?? x h).
  55 intros;
  56 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
  57 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
  58 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
  59 cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
  60   intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
  61   apply (le_transitive ???? (H7 0)); simplify;
  62   cases (H1 i); assumption;] clear H3;
  63 cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
  64   intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
  65   apply (le_transitive ????? (H7 0)); simplify;
  66   cases (H1 i); assumption;] clear H2;
  67 split;
  68 [1: cases Hx; cases H3; cases Hy; cases H7; split;
  69     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
  70     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
  71 |2: intros 3 (h);
  72     letin X ≝ (sig_in ?? x h);
  73     letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
  74     letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
  75     letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
  76     apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
  77     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
  78         [apply (H5 0);|apply (H7 0)]
  79     |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
  80         cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
  81         exists [apply w] apply H7;
  82     |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
  83         cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
  84         exists [apply w] apply H7;]]
  85 qed.
  86
  87
  88 (* Theorem 3.9 *)
  89 theorem lebesgue_se:
  90   ∀C:ordered_uniform_space.property_sigma C →
  91    (∀l,u:C.exhaustive {[l,u]}) →
  92     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
  93      ∀x:C.a order_converges x →
  94       x ∈ [l,u] ∧
  95       ∀h:x ∈ [l,u]. (* manca il pullback? *)
  96        uniform_converge
  97         (uniform_space_OF_ordered_uniform_space
  98          (segment_ordered_uniform_space C l u))
  99         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
 100         (sig_in ?? x h).
 101 intros (C S);
 102 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
 103 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
 104 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ (% → % → ?); intros;
 105 cut (∀i.xi i ∈ [l,u]) as Hxi; [2:
 106   intros; split; [2:apply H3] cases (Hxy i) (H5 _); cases H5 (H7 _);
 107   apply (le_transitive ???? (H7 0)); simplify;
 108   cases (H1 i); assumption;] clear H3;
 109 cut (∀i.yi i ∈ [l,u]) as Hyi; [2:
 110   intros; split; [apply H2] cases (Hxy i) (_ H5); cases H5 (H7 _);
 111   apply (le_transitive ????? (H7 0)); simplify;
 112   cases (H1 i); assumption;] clear H2;
 113 split;
 114 [1: cases Hx; cases H3; cases Hy; cases H7; split;
 115     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
 116     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
 117 |2: intros 3;
 118     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
 119     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
 120     letin X ≝ (sig_in ?? x h);
 121     letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
 122     letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
 123     letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
 124     apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
 125     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
 126         [apply (H5 0);|apply (H7 0)]
 127     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
 128         apply (H4 h);
 129     |3: cases (restrict_uniform_convergence_downarrow ? S ?? (H l u) Yi x Hy);
 130         apply (H4 h);]]
 131 qed.