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