Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: taylors.pvs Sprache: PVS

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.