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