helm/software/matita/contribs/dama/dama_duality/limit.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 "infsup.ma".
  16
  17 definition shift ≝ λT:Type.λs:sequence T.λk:nat.λn.s (n+k).
  18
  19 (* 3.28 *)
  20 definition limsup ≝
  21   λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E.
  22     (∀k.(alpha k) is_strong_sup (shift ? xn k) in E) ∧
  23      x is_strong_inf alpha in E.
  24
  25 notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}.
  26 notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}.
  27 notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
  28 notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
  29
  30 interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
  31 interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).
  32
  33 (* 3.29 *)
  34 definition lim ≝
  35   λE:excess.λxn:sequence E.λx:E. x is_limsup xn in E ∧ x is_liminf xn in E.
  36
  37 notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
  38 notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
  39 interpretation "Excess lim" 'lim e s x = (lim e s x).
  40
  41 lemma sup_decreasing:
  42   ∀E:excess.∀xn:sequence E.
  43    ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn in E) →
  44      alpha is_decreasing in E.
  45 intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
  46 intro r;
  47 elim (H r) (H1r H2r);
  48 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
  49 intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr;
  50 cases (H1r w Hw);
  51 qed.
  52
  53 include "tend.ma".
  54 include "metric_lattice.ma".
  55
  56 (* 3.30 *)
  57 lemma lim_tends:
  58   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
  59     x is_lim xn in ml → xn ⇝ x.
  60 intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;
  61 cases Hl (e1 e2); cases e1 (an Han); cases e2 (bn Hbn); clear Hl e1 e2;
  62 cases Han (SSan SIxan); cases Hbn (SSbn SIxbn); clear Han Hbn;
  63 cases SIxan (LBxan Hxg); cases SIxbn (UPxbn Hxl); clear SIxbn SIxan;
  64 change in UPxbn:(%) with (x is_lower_bound bn in ml);
  65 unfold upper_bound in UPxbn LBxan; change
  66 intros (e He);
  67 (* 2.6 OC *)