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.