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