SSL limit_real_vect2.pvs  Sprache: unbekannt

limit_real_vect2[ T : TYPE FROM real ]: THEORY
BEGIN

  IMPORTING vectors@distance_2D, vect_fun_ops_rv[T],
            reals@abs_lems

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


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

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

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

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

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

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

  convergence(f, a, l) : bool = 
%%        (FORALL e: EXISTS x: abs(x - a) < e) AND   % a has a ball containing T values
 FORALL epsilon : EXISTS delta : 
     FORALL x: abs(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_const : LEMMA convergence(const_vfun(b), a, 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)

  const_fun_convergent: LEMMA convergent?(const_vfun(b), 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)

%   %-----------------------------
%   %  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_real_vect2