helm/software/matita/dama/infsup.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 "sandwich_corollary.ma".
  16
  17 (* 3.19 *)
  18 definition supremum ≝
  19   λR.λml:mlattice R.λxn:sequence ml.λx:ml.
  20     increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
  21
  22 definition infimum ≝
  23   λR.λml:mlattice R.λxn:sequence ml.λx:ml.
  24     decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
  25
  26 (* 3.20 *)
  27 lemma supremum_uniq:
  28   ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn →
  29    ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
  30 intros (R ml xn Hxn x y Sx Sy);
  31 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
  32 apply (tends_uniq ?? xn ?? Hx Hy);
  33 qed.
  34
  35 definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
  36  λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
  37
  38 definition ank ≝
  39   λR.λml:mlattice R.λxn:sequence ml.λk:nat.
  40     let rec ank_aux (i : nat) ≝
  41       match i with
  42       [ O ⇒ (shift ?? xn k) O
  43       | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
  44     in ank_aux.
  45
  46 notation < "'a'\sup k" non associative with precedence 50 for
  47  @{ 'ank $x $k }.
  48
  49 interpretation "ank" 'ank x k =
  50  (cic:/matita/infsup/ank.con _ _ x k).
  51
  52 notation < "'a'(k \atop n)" non associative with precedence 50 for
  53  @{ 'ank2 $x $k $n }.
  54
  55 interpretation "ank2" 'ank2 x k n =
  56  (cic:/matita/infsup/ank.con _ _ x k n).
  57
  58 definition bnk ≝
  59   λR.λml:mlattice R.λxn:sequence ml.λk:nat.
  60     let rec bnk_aux (i : nat) ≝
  61       match i with
  62       [ O ⇒ (shift ?? xn k) O
  63       | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
  64     in bnk_aux.
  65
  66 notation < "'b'\sup k" non associative with precedence 50 for
  67  @{ 'bnk $x $k }.
  68
  69 interpretation "bnk" 'bnk x k =
  70  (cic:/matita/infsup/bnk.con _ _ x k).
  71
  72 notation < "('b' \sup k) \sub n" non associative with precedence 50 for
  73  @{ 'bnk2 $x $k $n }.
  74
  75 interpretation "bnk2" 'bnk2 x k n =
  76  (cic:/matita/infsup/bnk.con _ _ x k n).
  77
  78 lemma ank_decreasing:
  79   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
  80 intros (R ml xn k); unfold; intro n; simplify; apply lem;
  81 qed.
  82
  83 (* 3.26 *)
  84 lemma ankS:
  85   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
  86    ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
  87 intros (R ml xn k n); elim n; simplify; [apply meet_comm]
  88 simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
  89 apply (Eq≈ ? (meet_assoc ????));
  90 apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
  91 apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
  92 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
  93 apply meet_comm;
  94 qed.
  95
  96 lemma bnkS:
  97   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
  98    ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
  99 intros (R ml xn k n); elim n; simplify; [apply join_comm]
 100 simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
 101 apply (Eq≈ ? (join_assoc ????));
 102 apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
 103 apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
 104 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
 105 apply join_comm;
 106 qed.
 107
 108 lemma le_asnk_ansk:
 109   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
 110    (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
 111 intros (R ml xn k n);
 112 apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
 113 qed.
 114
 115 lemma le_bnsk_bsnk:
 116   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
 117    (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
 118 intros (R ml xn k n);
 119 apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????));
 120 apply (Le≫ ? (join_comm ???));
 121 apply lej;
 122 qed.
 123
 124
 125 (* 3.27 *)
 126 lemma inf_increasing:
 127   ∀R.∀ml:mlattice R.∀xn:sequence ml.
 128    ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) →
 129      increasing ml alpha.
 130 intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold;
 131 intro r;
 132 elim (H r) (H1r H2r);
 133 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
 134 intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
 135 lapply (H1r (S w)) as Hsw; clear H1r;
 136 lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
 137 cases (H Hw);
 138 qed.
 139
 140 lemma sup_decreasing:
 141   ∀R.∀ml:mlattice R.∀xn:sequence ml.
 142    ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) →
 143      decreasing ml alpha.
 144 intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
 145 intro r;
 146 elim (H r) (H1r H2r);
 147 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
 148 intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
 149 lapply (H1r (S w)) as Hsw; clear H1r;
 150 lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
 151 cases (H Hw);
 152 qed.
 153
 154 (* 3.28 *)
 155 definition liminf ≝
 156   λR.λml:mlattice R.λxn:sequence ml.λx:ml.
 157     ∃alpha:sequence ml.
 158       (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
 159
 160 definition limsup ≝
 161   λR.λml:mlattice R.λxn:sequence ml.λx:ml.
 162     ∃alpha:sequence ml.
 163       (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
 164
 165 (* 3.29 *)
 166 alias symbol "and" = "constructive and".
 167 definition lim ≝
 168   λR.λml:mlattice R.λxn:sequence ml.λx:ml.
 169    (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
 170
 171 (* 3.30 *)
 172 lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
 173    lim ?? xn x → xn ⇝ x.
 174 intros (R ml xn x Hl);
 175 unfold in Hl; unfold limsup in Hl; unfold liminf in Hl;
 176 (* decompose; *)
 177 elim Hl (low Hl_); clear Hl;
 178 elim Hl_ (up Hl); clear Hl_;
 179 elim Hl (Hl_ E1); clear Hl;
 180 elim Hl_ (Hl E2); clear Hl_;
 181 elim Hl (H1 H2); clear Hl;
 182 elim H1 (alpha Halpha); clear H1;
 183 elim H2 (beta Hbeta); clear H2;
 184 apply (sandwich ?? alpha beta);
 185 [1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
 186     lapply (sup_increasing ????? Ha6) as Ha7;
 187
 188     unfold strong_sup in Halpha Hbeta;
 189     unfold strong_inf in Halpha Hbeta;
 190     unfold lower_bound in Halpha Hbeta;
 191     unfold upper_bound in Halpha Hbeta;
 192     elim (Halpha m) (Ha5 Ha6); clear Halpha;
 193     elim Ha5 (Ha1 Ha2); clear Ha5;
 194     elim Ha6 (Ha3 Ha4); clear Ha6;
 195     split;
 196     [1: intro H; elim (Ha2 ? H) (w H1);
 197         elim (Ha4 ? H1);
 198
 199
 200
 201