helm/software/matita/library/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 (* NOT DUALIZED *)
  20 alias symbol "low" = "lower".
  21 alias id "le" = "cic:/matita/dama/ordered_set/le.con".
  22 lemma order_converges_bigger_lowsegment:
  23   ∀C:ordered_set.
  24    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
  25      ∀x:C.∀p:order_converge C a x.
  26        ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
  27 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
  28 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
  29 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
  30 intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
  31 lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
  32 qed.
  33
  34 alias symbol "upp" = "uppper".
  35 alias symbol "leq" = "Ordered set less or equal than".
  36 lemma order_converges_smaller_upsegment:
  37   ∀C:ordered_set.
  38    ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
  39      ∀x:C.∀p:order_converge C a x.
  40        ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
  41 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
  42 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
  43 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
  44 intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K;
  45 cases (cases_in_segment ? s ? K); apply H1; apply Hw;
  46 qed.
  47
  48 (* Theorem 3.10 *)
  49 theorem lebesgue_oc:
  50   ∀C:ordered_uniform_space.
  51    (∀s:‡C.order_continuity {[s]}) →
  52     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
  53      ∀x:C.a order_converges x →
  54       x ∈ s ∧
  55       ∀h:x ∈ s.
  56        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
  57 intros;
  58 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
  59 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
  60 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
  61 cut (∀i.xi i ∈ s) as Hxi; [2:
  62   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
  63   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
  64   simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
  65 cut (∀i.yi i ∈ s) as Hyi; [2:
  66   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
  67   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
  68   apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
  69 split;
  70 [1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
  71 |2: intros 3 (h);
  72     letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
  73     letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
  74     letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
  75     apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
  76     [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
  77         [apply (l2sl_ ? s (Xi j) (Ai j) (H5 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H7 0))]
  78     |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl_ ? s (Xi i) (Xi (S i)) (H3 i));]
  79         cases H4; split; [intro i; apply (l2sl_ ? s (Xi i) ≪x,h≫ (H5 i))]
  80         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s ? y Hy)]
  81         exists [apply w] apply (x2sx_ ? s (Xi w) y H7);
  82     |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl_ ? s (Yi (S i))  (Yi i) (H3 i));]
  83         cases H4; split; [intro i; apply (l2sl_ ? s ≪x,h≫ (Yi i) (H5 i))]
  84         intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s y ≪x,h≫ Hy)]
  85         exists [apply w] apply (x2sx_ ? s y (Yi w) H7);]]
  86 qed.
  87
  88
  89 (* Theorem 3.9 *)
  90 theorem lebesgue_se:
  91   ∀C:ordered_uniform_space.property_sigma C →
  92    (∀s:‡C.exhaustive {[s]}) →
  93     ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
  94      ∀x:C.a order_converges x →
  95       x ∈ s ∧
  96       ∀h:x ∈ s.
  97        uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
  98 intros (C S);
  99 generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
 100 generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
 101 cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
 102 cut (∀i.xi i ∈ s) as Hxi; [2:
 103   intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
 104   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
 105   simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
 106 cut (∀i.yi i ∈ s) as Hyi; [2:
 107   intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
 108   lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
 109   apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
 110 letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
 111 letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
 112 cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
 113 cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
 114 split; [1: assumption]
 115 intros 3;
 116 lapply (uparrow_upperlocated  xi x Hx)as Ux;
 117 lapply (downarrow_lowerlocated  yi x Hy)as Uy;
 118 letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
 119 apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
 120 intro j; cases (Hxy j); cases H7; cases H8; split;
 121 [apply (l2sl_ ? s (Xi j) (Ai j) (H9 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H11 0))]
 122 qed.
 123
 124
 125