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

quality93%

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