Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/lnexp_fnd/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 28.9.2014 mit Größe 1 kB image not shown  

SSL exp_series.pvs   Interaktion und
PortierbarkeitPVS

 
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], ints@factorial,
              convergence_special,
       reals@polynomials

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

   AUTO_REWRITE+ sigma_0_neg


   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: LEMMA 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) 

   exp_estimate_increasing: LEMMA
     -1 <= x AND x<=y IMPLIES
     exp_estimate(x,n) <= exp_estimate(y,n)

   exp_estimate_positive: LEMMA
     n>=2 AND -1 <= x IMPLIES
     exp_estimate(x,n)>0

   exp_estimate_0: LEMMA
     exp_estimate(0,n) = 1


END exp_series

85%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.