products/sources/formale Sprachen/Delphi/Agenda 1.1 image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: limit_vect3_real.pvs   Sprache: PVS

limit_vect3_real: THEORY
BEGIN

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

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

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

  convergence(f, a, l) : bool = 
 FORALL epsilon : EXISTS delta : 
     FORALL x: %%% 0 < norm(x-a) AND
                      norm(x-a) < delta          %% AND x in dom(f)
                 IMPLIES abs(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)


  cv_inv   : LEMMA convergence(g, a, l) AND l /= 0
                     IMPLIES convergence(1 / g, a, 1 / l)

  cv_div   : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0
                     IMPLIES convergence(f / g, a, l1 / l2)

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

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

  lim(f, (x0 : {a | convergent?(f, a)})) : real =  
        epsilon(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)
        
  inv_fun_convergent  : LEMMA convergent?(g, a) AND lim(g, a) /= 0
                                 IMPLIES convergent?(1/g, a)

  div_fun_convergent  : LEMMA convergent?(f, a) AND convergent?(g, a)
                                AND lim(g, a) /= 0 IMPLIES convergent?(f / g, 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)
        
  lim_inv_fun      : LEMMA convergent?(g, a) AND lim(g, a) /= 0
                             IMPLIES lim(1/g, a) = 1/lim(g, a)

  lim_div_fun      : LEMMA convergent?(f, a) AND convergent?(g, a) AND lim(g, a) /= 0
                             IMPLIES lim(f / g, a) = lim(f, a)/lim(g, 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_vect3_real

[ zur Elbe Produktseite wechseln0.17Quellennavigators  Analyse erneut starten  ]