Quelle  limit_vect2_vect2.pvs   Sprache: PVS

limit_vect2_vect2: THEORY
BEGIN

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

  f, f1, f2: VAR [ Vect2 -> Vect2]
  g : VAR [Vect2 -> nzreal]
  epsilon, delta : VAR posreal
  a,x,v: VAR Vect2
  l,l1,l2,b,c,y1,y2: VAR Vect2


  const_fun(v) : [Vect2 -> Vect2] = LAMBDA x : v ;

  +(f1, f2) : [Vect2 -> Vect2] = LAMBDA x : f1(x) + f2(x);
 
  -(f1)     : [Vect2 -> Vect2] = LAMBDA x : -f1(x);

  -(f1, f2) : [Vect2 -> Vect2] = LAMBDA x : f1(x) - f2(x);

%%%  *(f1, f2) : [Vect2 -> Vect2] = LAMBDA x : f1(x) * f2(x);  


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

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

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

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

  %-------------------------------------------
  %  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_prod  : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
%                      IMPLIES convergence(f1 * f2, a, l1 * l2)

  cv_const : LEMMA convergence(const_fun(b), v, b)

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

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

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

  lim(f, (x0 : {a | convergent?(f, a)})) : Vect2 =  
        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 convergence 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(b), v)
        
%  scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(b * 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(b), v) = b

%   lim_scal_fun     : LEMMA convergent?(f, a) 
%                              IMPLIES lim(b * f, a) = b * lim(f, a)
        
%   %-----------------------------
%   %  Limit preserve order
%   %-----------------------------

%   convergence_order : LEMMA
%  FORALL f1, f2, a, l1, l2 :
%  convergence(f1, a, l1)
%      AND convergence(f2, a, l2)
%      AND (FORALL x : f1(x) <= f2(x))
%  IMPLIES l1 <= l2
  

%   %-------------------------------------------
%   %  Bounds on function are bounds on limits
%   %-------------------------------------------

%   convergence_lower_bound : COROLLARY
%  FORALL f, b, a, l :
%  convergence(f, a, l)
%      AND (FORALL x : b <= f(x))
%  IMPLIES b <= l

%   convergence_upper_bound : COROLLARY
%  FORALL f, b, a, l :
%  convergence(f, a, l)
%      AND (FORALL x : f(x) <= b)
%  IMPLIES l <= b


%   %--------------------
%   %  Bounds on limits
%   %--------------------

%   lim_le1 : LEMMA
%         convergent?(f, a) AND (FORALL x : f(x) <= b) IMPLIES lim(f, a) <= b

%   lim_ge1 : LEMMA
%         convergent?(f, a) AND (FORALL x : f(x) >= b) IMPLIES lim(f, a) >= b
  
%   lim_order1 : LEMMA convergent?(f1, a) AND convergent?(f2, a)
%                      AND (FORALL x : f1(x) <= f2(x)) 
%                          IMPLIES lim(f1, a) <= lim(f2, a)

END limit_vect2_vect2