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 le x_i e y_i stanno o no nel segmento?
  20
  21 (* Theorem 3.10 *)
  22 theorem lebesgue:
  23   ∀C:ordered_uniform_space.
  24    (∀l,u:C.order_continuity {[l,u]}) →
  25     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
  26      ∀x:C.a order_converges x →
  27       x ∈ [l,u] ∧
  28       ∀h:x ∈ [l,u]. (* manca il pullback? *)
  29        uniform_converge
  30         (uniform_space_OF_ordered_uniform_space
  31          (segment_ordered_uniform_space C l u))
  32         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
  33         (sig_in ?? x h).
  34 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5;
  35 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
  36 split;
  37 [2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h));
  38
  39
  40 (* Theorem 3.9 *)
  41 theorem lebesgue:
  42   ∀C:ordered_uniform_space.property_sigma C →
  43    (∀l,u:C.exhaustive {[l,u]}) →
  44     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u].
  45      ∀x:C.a order_converges x →
  46       x ∈ [l,u] ∧
  47       ∀h:x ∈ [l,u]. (* manca il pullback? *)
  48        uniform_converge
  49         (uniform_space_OF_ordered_uniform_space
  50          (segment_ordered_uniform_space C l u))
  51         (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))
  52         (sig_in ?? x h).
  53 intros; cases H3 (xi H4); cases H4 (yi H5); cases H5; cases H6; cases H8;
  54 cases H9; cases H10; cases H11; clear H3 H4 H5 H6 H8 H9 H10 H11 H15 H16;
  55 lapply (uparrow_upperlocated ? xi x)as Ux;[2: split; assumption]
  56 lapply (downarrow_lowerlocated ? yi x)as Uy;[2: split; assumption]
  57 cases (restrict_uniform_convergence ? H ?? (H1 l u) (λn:nat.sig_in ?? (a n) (H2 n)) x);
  58 [ split; assumption]
  59 split; simplify;
  60  [1: intro;  cases (H7 n); cases H3;
  61
  62
  63  lapply (sandwich ? x xi yi a );
  64   [2: intro; cases (H7 i); cases H3; cases H4; split[apply (H5 0)|apply (H8 0)]
  65   |3: intros 2;
  66       cases (restrict_uniform_convergence ? H ?? (H1 l u) ? x);
  67       [1:
  68
  69 lapply (restrict_uniform_convergence ? H ?? (H1 l u)
  70          (λn:nat.sig_in ?? (a n) (H2 n)) x);
  71   [2:split; assumption]