Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/lnexp_fnd/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

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], 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

quality85%

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