Datei: Musik Download des Quellcode-Bibliothek Quellennavigators
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Delphi/Autor 0.7/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 4.1.2008 mit Größe 2 kB image not shown  

SSL lim_of_functions.pvs   Sprache: PVS

 
lim_of_functions [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Limit of a functions [T -> real] at a point a   %
%
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING convergence_functions

  %------------------------------------------------
  %  Subtype of reals where the limit makes sense
  %------------------------------------------------

  a, b, l, l1, l2 : VAR real
  c : VAR (adh[T](fullset[real]))
  f, f1, f2 : VAR [ T -> real]
  g : VAR [T -> nzreal]
  epsilon, delta : VAR posreal
  x : VAR T

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

  convergence(f, a, l) : bool = convergence(f, fullset[real], a, l)

  convergence_def : LEMMA
        FORALL f, a, l :
            convergence(f, a, l)
        IFF
            adh[T](fullset[real])(a)
        AND FORALL epsilon : EXISTS delta :
                FORALL x : abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon


  adherence_fullset : LEMMA adh[T](fullset[real])(x)

  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_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), c, b)

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

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

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

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

  cv_identity: LEMMA convergence(I[T], c, c)
        
  cv_abs   : LEMMA convergence(abs, c, abs(c))
        
  conv_0_0_abs: LEMMA convergence(f, 0, 0) IFF convergence(abs(f), 0, 0)


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

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

%  lim(f, (x0 : {a | convergent?(f, a)})) : real =  
%        choose(LAMBDA l : convergence(f, x0, l))


  lim(f, (x0 : {a | convergent?(f, a)})) : {l: real |  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)

  lim_e_del: LEMMA convergent?(f, a) IMPLIES
    (lim(f, a) = l IFF FORALL (e: posreal): EXISTS (del: posreal): FORALL (x: T):
                           abs(x-a) < del IMPLIES abs(f(x) - l) < e)

  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), c)
        
  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)

  convergent_identity : LEMMA convergent?(I[T], c)


  %----------------------------
  %  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), c) = 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)

  lim_identity : LEMMA lim(I[T], c) = c
  



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

  E : VAR setof[real]

  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)

  lim_le2    : LEMMA convergent?(f, a) AND adh[T](E)(a) AND 
                     (FORALL x : E(x) IMPLIES f(x) <= b) 
                         IMPLIES lim(f, a) <= b

  lim_ge2    : LEMMA convergent?(f, a) AND adh[T](E)(a) AND 
                     (FORALL x : E(x) IMPLIES f(x) >= b) 
                         IMPLIES lim(f, a) >= b

  lim_order2 : LEMMA convergent?(f1, a) AND convergent?(f2, a)  AND adh[T](E)(a)
                     AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
                         IMPLIES lim(f1, a) <= lim(f2, a)


  AUTO_REWRITE+ adherence_fullset



END lim_of_functions

96%


¤ Dauer der Verarbeitung: 0.11 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders