Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: exp_series.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.0 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.