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 foo:
  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 ≤ (match p with [ex_introT xi _ ⇒ xi] j).
  24 intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
  25 cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
  26 cases H2; clear H2;  intro; cases (H5 ? H2);
  27 cases (H (w2+j)); apply (H8 H6);
  28 qed.
  29
  30
  31 (* Theorem 3.10 *)
  32 theorem lebesgue:
  33   ∀C:ordered_uniform_space.
  34    (∀l,u:C.order_continuity {[l,u]}) →
  35     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
  36      ∀x:C.a order_converges x →
  37       x ∈ [l,u] ∧
  38       ∀h:x ∈ [l,u]. (* manca il pullback? *)
  39        uniform_converge
  40         (uniform_space_OF_ordered_uniform_space
  41          (segment_ordered_uniform_space C l u))
  42         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
  43         (sig_in ?? x h).
  44 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5;
  45 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
  46 split;
  47 [2: intro h;
  48   cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h));
  49
  50
  51 (* Theorem 3.9 *)
  52 theorem lebesgue:
  53   ∀C:ordered_uniform_space.property_sigma C →
  54    (∀l,u:C.exhaustive {[l,u]}) →
  55     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
  56      ∀x:C.a order_converges x →
  57       x ∈ [l,u] ∧
  58       ∀h:x ∈ [l,u]. (* manca il pullback? *)
  59        uniform_converge
  60         (uniform_space_OF_ordered_uniform_space
  61          (segment_ordered_uniform_space C l u))
  62         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
  63         (sig_in ?? x h).
  64 intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8;
  65 cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
  66 lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
  67 lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
  68 cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x);
  69 [ split; assumption]
  70 split; simplify;
  71  [1: intro;  cases (H7 n); cases H3;
  72
  73
  74  lapply (sandwich ? x xi yi a );
  75   [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
  76   |3: intros 2;
  77       cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x);
  78       [1:
  79
  80 lapply (restrict_uniform_convergence ? H ?? (H1 l u)
  81          (λn:nat.sig_in ?? (a n) (H2 n)) x);
  82   [2:split; assumption]