Quelle taylor_series.pvs Sprache: PVS

taylor_series[T: TYPE+ from real]: THEORY
%----------------------------------------------------------------------------
%
%                        n-1
%                     ----
%                               =   \     (k+1)*a(k+1)*x^k
%                     /
%                     ----
%                     k = 0
%
% The intention here is that one passes in the domain of convergence [T]
% of the power series.  This will either be all of the reals or {x| -R < x < R}
% where R is the range of convergence.  Most of the lemmas assume
% convergence of the power series a: conv_powerseries?(a) =
%     (FORALL (x: T): convergent?(powerseries(a)(x)))
%
%
% Author: Ricky W. Butler        7/8/2004
%
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING  %% T is either "real" or a open ball of radius R about 0
     IMPORTING analysis@deriv_domain_def

     connected_domain : ASSUMPTION connected?[T]

     not_one_element : ASSUMPTION not_one_element?[T]

     open            : ASSUMPTION
         FORALL (x : T) : EXISTS (delta : posreal): FORALL (y: real):
                            abs(x-y) < delta IMPLIES T_pred(y)

     ball: ASSUMPTION FORALL (x: T): T_pred(x) IMPLIES T_pred(-x)

   ENDASSUMING

   T_pred_0: LEMMA T_pred(0)

   IMPORTING analysis@deriv_domain_def, power_series_deriv[T]

   deriv_domain: LEMMA  deriv_domain?[T]

   x,x0: VAR T
   k,n: VAR nat
   a: VAR sequence[real]
   t: VAR real

   epsilon: VAR posreal

   f: VAR [T -> real]

   Inf_sum_0: LEMMA conv_powerseries?[T](a) IMPLIES
                        Inf_sum(a)(0) = a(0)

   nderivseq(n,a): sequence[real] =
             (LAMBDA (k: nat): factorial(k+n)/factorial(k)*a(k+n))

   nderivseq_lem: LEMMA nderivseq(n+1, a) =
                        nderivseq(n,derivseq(a))

   conv_nderivseq: LEMMA conv_powerseries?(a) IMPLIES
                             conv_powerseries?[T](nderivseq(n, a))

   Inf_sum_derivable_n_times: LEMMA  conv_powerseries?(a) IMPLIES
                                 derivable_n_times?[T](Inf_sum[T](a), n)

   nderiv_Inf_sum: THEOREM conv_powerseries?(a) IMPLIES
                       nderiv[T](n,Inf_sum(a)) = Inf_sum(nderivseq(n,a))

   Taylor_expansion: LEMMA FORALL n: conv_powerseries?[T](a) AND
                                     f = Inf_sum(a)
                              IMPLIES derivable_n_times?(f,n) AND
                                      factorial(n)*a(n) = nderiv(n,f)(0)

   Taylor_seq(f:(inf_deriv_fun?[T]))(n): real =
                                        nderiv(n,f)(0)/factorial(n)

   Taylor_seq_term: LEMMA inf_deriv_fun?(f) IMPLIES
                         (LAMBDA n: IF n = 0 THEN f(0)
                                    ELSE Taylor_seq(f)(n)*x^n
                                    ENDIF) = Taylor_term(f,0,x)

%  ---- GET_C returns the const c from Taylor's Theorem -----

   GET_C(f:(inf_deriv_fun?[T]), x: T, k: nat): {c: between[T](0, x) |
                   powerseries(Taylor_seq(f))(x)(k) =
                        f(x) - Taylor_rem(k, f, 0, x, c)}

   is_taylor_prep: LEMMA inf_deriv_fun?(f) AND
                      (FORALL (x:T):
                        convergent?(LAMBDA n: Taylor_rem(n,f,0,x,GET_C(f,x,n))))
                     IMPLIES
                        conv_powerseries?[T](Taylor_seq(f))

   is_taylor: LEMMA  inf_deriv_fun?(f) AND
                      (FORALL (x:T):
                     convergence(LAMBDA n: Taylor_rem(n,f,0,x,GET_C(f,x,n)),0))
                  IMPLIES
                        f = Inf_sum(Taylor_seq(f))

END taylor_series

quality67%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

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.