Quelle  exp_series.pvs   Sprache: PVS

exp_series: THEORY
%----------------------------------------------------------------------------
%
%  Series expansion for Exponential Function
%
%  Author: Ricky W. Butler              NASA Langley Research Center
%
%  Note.  See ln_exp_series_alt for an alternate formulation
%----------------------------------------------------------------------------
BEGIN
   IMPORTING  ln_exp
%              series@taylor_series[real], 
%              convergence_special

   IMPORTING reals@sigma_nat, reals@factorial, taylor_help

   x: VAR real
   n,m: VAR nat
   a: VAR sequence[real]
   l,t: VAR real


   exp_seq(n): real = 1/factorial(n)

%   nderiv_exp: LEMMA derivable_n_times(exp, n)
%                     AND nderiv(n, exp) = exp

%   exp_inf_deriv: LEMMA inf_deriv_fun?[real](exp)

%   exp_series_prep: LEMMA 
%                     convergence(LAMBDA n: Taylor_rem(n,exp,0,x,
%                                           GET_C(exp,x,n)),0)

%   conv_exp: LEMMA conv_powerseries?[real](exp_seq)

%   exp_series: THEOREM exp = Inf_sum(exp_seq)  % lim n->inf  Sum  x^n/n!


   exp_estimate(x:real,n:nat):real = 
                1 + sigma(1,n,(LAMBDA (nn:nat): x^nn/factorial(nn)))


   exp_taylors: AXIOM EXISTS (c: between[real](0,x)):
                           exp(x) = exp_estimate(x,n)
                                        + exp(c)*x^(n+1)/factorial(n+1)

   exp_taylors_err: LEMMA abs(exp(x)-exp_estimate(x,n)) 
                                <= max(exp(x),1)*abs(x)^(n+1)/factorial(n+1)


END exp_series