limit_vect.pvs

limit_vect[n,m:posnat]: THEORY
BEGIN

  IMPORTING vectors@vectors, 
            reals@abs_lems, 
            analysis@epsilon_lemmas

  f, f1, f2: VAR [ Vector[n] -> Vector[m] ]
  a,b,x,v : VAR Vector[n]
  l,l1,l2 : VAR Vector[m]
  epsilon, delta : VAR posreal
  k : VAR real

  ;+(f1, f2)(v) : MACRO Vector[m] = f1(v) + f2(v)
 
  ;-(f)(v): MACRO Vector[m] = -f(v)

  ;-(f1, f2)(v) : MACRO Vector[m] = f1(v) - f2(v)

  ;*(k, f)(v) : MACRO Vector[m] = k*f(v)

  ;*(f1,f2)(v) : MACRO real = f1(v)*f2(v)

  const_fun(l)(x): Vector[m] = l


  %---------------------------------------------------
  %  Convergence of f at a point a towards a limit l
  %--------------------------------------------------

  convergence(f, a, l): bool = 
 FORALL epsilon : EXISTS delta : 
     FORALL v: norm(v-a) < delta        
                 IMPLIES norm(f(v) - l) < epsilon

  cv_unique : LEMMA 
    convergence(f, a, l1) AND convergence(f, a, l2)
      IMPLIES l1 = l2

  cv_in_domain : LEMMA 
    convergence(f, a, l) 
      IMPLIES l = f(a)

  %-------------------------------------------
  %  convergence and operations on functions
  %-------------------------------------------

  cv_sum   : LEMMA 
    convergence(f1, a, l1) AND convergence(f2, a, l2)
      IMPLIES convergence(f1 + f2, a, l1 + l2)

  cv_neg   : LEMMA 
    convergence(f, a, l)
      IMPLIES convergence(-f, a, -l)

  cv_diff  : LEMMA 
    convergence(f1, a, l1) AND convergence(f2, a, l2)
      IMPLIES convergence(f1 - f2, a, l1 - l2)

  cv_const : LEMMA convergence(LAMBDA v: l, a, l)

  cv_scal  : LEMMA 
    convergence(f, a, l) 
      IMPLIES convergence(k*f, a, k*l)

  %-------------------------
  %  f is convergent at a    
  %-------------------------

  convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)

  lim(f, (x0 : {a | convergent?(f, a)})) : Vector[m] =  
        choose(LAMBDA l : convergence(f, x0, l))

  lim_fun_lemma   : LEMMA FORALL f, (x0 : {a | convergent?(f, a)}) :
                          convergence(f, x0, lim(f, x0))

  lim_fun_def     : LEMMA FORALL f, l, (x0 : {a | convergent?(f, a)}) :
                             lim(f, x0) = l IFF convergence(f, x0, l)

  convergence_equiv    : LEMMA convergence(f, a, l) IFF 
                                  convergent?(f, a) AND lim(f, a) = l
       
  convergent_in_domain : LEMMA convergent?(f, x) IFF convergence(f, x, f(x))
       
  lim_in_domain        : LEMMA convergent?(f, x) IMPLIES lim(f, x) = f(x)
       

 %------------------------------------------
 %  Operations preserving convergnce at a 
 %------------------------------------------

  sum_fun_convergent  : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                                IMPLIES convergent?(f1 + f2, a)

  neg_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(- f, a)
       
  diff_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                                IMPLIES convergent?(f1 - f2, a)

%    prod_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                                  IMPLIES convergent?(f1 * f2, a)

  const_fun_convergent: LEMMA convergent?(const_fun(l), a)
       
  scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(k * f, a)
        
  %----------------------------
  %  Same things with lim(a)
  %----------------------------
  lim_sum_fun      : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                             IMPLIES lim(f1 + f2, a) = lim(f1, a) + lim(f2, a)

  lim_neg_fun : LEMMA convergent?(f, a) 
                             IMPLIES lim(- f, a) = - lim(f, a)
       
  lim_diff_fun     : LEMMA convergent?(f1, a) AND convergent?(f2, a)
                             IMPLIES lim(f1 - f2, a) = lim(f1, a) - lim(f2, a)

%    lim_prod_fun     : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                               IMPLIES lim(f1 * f2, a) = lim(f1, a) * lim(f2, a)

  lim_const_fun    : LEMMA lim(const_fun(l), a) = l

   lim_scal_fun     : LEMMA convergent?(f, a) 
                              IMPLIES lim(k * f, a) = k * lim(f, a)
        
END limit_vect