Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/   (Wiener Entwicklungsmethode ©)  Datei vom 28.9.2014 mit Größe 3 kB image not shown  

SSL taylors.pvs   Interaktion und
PortierbarkeitPVS

 
taylors[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
% The Taylors theory establishes Taylor's Theorem (Rosenlicht Page 107)
%
%
% Developed  by Ricky W. Butler      NASA Langley Research Center
%               David Lester         Manchester University
% 
%      Version 1.0    last modified 10/30/00
%      version 1.1    Generalised for arbitrary interval T (DRL) 27/10/03
%   
%------------------------------------------------------------------------------

BEGIN

   ASSUMING
     IMPORTING deriv_domain_def

     connected_domain : ASSUMPTION connected?[T]
 
     not_one_element : ASSUMPTION not_one_element?[T]
 
   ENDASSUMING

   deriv_domain: LEMMA deriv_domain?[T]
   IMPORTING reals@sigma_nat, ints@factorial
   IMPORTING derivatives, nth_derivatives 
   IMPORTING derivative_props % need mean value theorem




   f:            VAR [T -> real]
   m, n, nn, ii: VAR nat
   x,xx,aa,bb:   VAR T
   Rn: VAR [T -> real]


%   fn: VAR [nat -> real]
%   nn: VAR negint
%   sigma_0_neg: LEMMA sigma(0,nn,fn) = 0
   AUTO_REWRITE+ sigma_0_neg


   sigma_derivable: LEMMA  FORALL (g: [T,nat -> real]):
                   (FORALL (ii: subrange(0,n)):
                          derivable?(LAMBDA aa: g(aa,ii))) IMPLIES
          derivable?[T](LAMBDA aa: sigma(0, n, (LAMBDA m: g(aa,m))))


   tay1: LEMMA derivable?((LAMBDA x: (bb - x) ^ n / factorial(n)))

   tay2: LEMMA derivable?(LAMBDA x: (bb - x)) AND 
               deriv(LAMBDA x: (bb - x)) = const_fun(-1)

   tay3: LEMMA derivable?(LAMBDA x: (bb - x) ^ (n+1)/factorial(n+1)) AND
               deriv(LAMBDA x: (bb - x) ^ (n+1)/factorial(n+1)) =
                      - (LAMBDA x: (bb - x) ^ n/factorial(n))

   deriv_sigma: LEMMA FORALL (FF: [T,nat -> real]): 
              (FORALL (ii: subrange(0,n)): derivable?(LAMBDA xx: FF(xx,ii)))
                IMPLIES
                      deriv(LAMBDA x: sigma(0,n,(LAMBDA n: FF(x,n)))) =
         (LAMBDA x: sigma(0,n,(LAMBDA ii: IF ii > n THEN 0 
                                          ELSE deriv(LAMBDA xx: FF(xx,ii))(x)
                                          ENDIF)))
   
   nderiv_term_derivable: LEMMA derivable_n_times?(f,n+1) IMPLIES
                   derivable?(LAMBDA (aa: T): 
                    IF n = 0 THEN f(aa) ELSE
                       nderiv(n, f)(aa) * (bb-aa)^n / factorial(n)
                    ENDIF)

   taylor_derivable: LEMMA derivable_n_times?(f,n+1) IMPLIES
          derivable?(LAMBDA aa: f(bb) -
              sigma(0, n,  LAMBDA nn:
                      IF nn > n  THEN 0
                      ELSIF nn = 0 THEN f(aa)
                      ELSE nderiv(nn,f)(aa) * (bb - aa)^nn / factorial(nn)
                      ENDIF))

   deriv_nderiv: LEMMA  derivable_n_times?(f, n+1) IMPLIES
                      deriv((LAMBDA xx: (nderiv(n, f)(xx)))) = nderiv(n+1, f)

   term_by_term_deriv: LEMMA derivable_n_times?(f, 1 + n) IMPLIES
        sigma(0, n,
               LAMBDA ii: IF ii > n THEN 0
                        ELSE deriv(LAMBDA xx: IF ii = 0 THEN f(xx) ELSE
                                         nderiv(ii, f)(xx) * (bb - xx) ^ ii /
                                                   factorial(ii) ENDIF) (x)
                        ENDIF)
                          = nderiv(1 + n, f)(x) * (bb - x) ^ n / factorial(n)



   taylor_lemma: LEMMA derivable_n_times?(f,n+1) AND 
                       Rn = (LAMBDA aa: f(bb) - 
                          sigma(0,n,(LAMBDA nn: IF nn > n THEN 0 
                            ELSIF nn = 0 THEN f(aa)
                            ELSE
                             nderiv(nn,f)(aa)*(bb-aa)^nn/factorial(nn) ENDIF)))
             IMPLIES
                deriv(Rn) = (LAMBDA x: -nderiv(n+1,f)(x)*(bb-x)^n/factorial(n))

   between(aa,bb): TYPE = {x: T | (aa < bb IMPLIES aa < x AND x < bb) AND
                                  (bb < aa  IMPLIES bb < x AND x < aa) AND
                                  (aa = bb IMPLIES x = aa)}

%  Note: if aa /= bb then between(aa,bb) is Open_interval(aa,bb) 

   Taylors: THEOREM derivable_n_times?(f,n+1) IMPLIES
               (EXISTS (c: between(aa,bb)): 
               f(bb) = sigma(0,n,(LAMBDA nn: IF nn > n THEN 0 
                                             ELSIF nn = 0 THEN f(aa) ELSE
                            nderiv(nn,f)(aa)*(bb-aa)^nn/factorial(nn) ENDIF))
                         + nderiv(n+1,f)(c)*(bb-aa)^(n+1)/factorial(n+1))


   Taylor_rem(n:nat,f:nderiv_fun[T](n+1),aa,bb,(c:between(aa,bb))): real = 
              nderiv(n+1,f)(c)*(bb-aa)^(n+1)/factorial(n+1)


%  --------- Infinitely Derivable Functions ---------

   inf_deriv_fun?(f): bool = (FORALL n: derivable_n_times?(f,n))

   Taylor_term(f:(inf_deriv_fun?),aa,bb)(n): real = 
                                   IF n = 0 THEN f(aa) ELSE
                                     nderiv(n,f)(aa)*(bb-aa)^n/factorial(n) 
                                   ENDIF

   Taylors_inf: THEOREM inf_deriv_fun?(f) IMPLIES
                        (EXISTS (c: between(aa,bb)): 
                           f(bb) = sigma(0,n,Taylor_term(f,aa,bb))
                                         + Taylor_rem(n,f,aa,bb,c))

END taylors



50%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.