Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ln_exp_series_alt.pvs Sprache: PVS

Original von: PVS^©

ln_exp_series_alt: THEORY
%------------------------------------------------------------------------------
%
% Alternate means of establishing infinite series for ln and exp
%
% Author: David Lester
%
%
%------------------------------------------------------------------------------
BEGIN

   real_gtm1_le1: NONEMPTY_TYPE = {x:real | -1 < x AND x <= 1} CONTAINING 0

   x:    VAR real
   px:   VAR posreal
   xgm1: VAR {x:real | x > -1}
   nzx:  VAR nzreal
   z:    VAR real_gtm1_le1
   n:    VAR nat

   IMPORTING ln_exp,
%             analysis@derivative_inverse,
%             series@nth_derivatives, series@taylors, series@series,
%             analysis@integral,
             reals@sqrt, reals@sigma_nat, reals@factorial, taylor_help

%    nderiv_ln: LEMMA derivable_n_times[posreal](ln,n)

%    ln_nderiv      : LEMMA nderiv[posreal](n,ln) = IF n = 0 THEN ln ELSE
%                         (LAMBDA (x:posreal): -factorial(n-1)/(-x)^n) ENDIF

   ln_estimate(x:real,n:nat):real
         = sigma(0,n,(LAMBDA (nn:nat): IF nn=0 THEN 0 ELSE -(-x)^nn/nn ENDIF))

%    ln_estimate_scaf1: LEMMA continuous((LAMBDA (t: posreal): (1-t)^n/t))

%    ln_estimate_scaf2: LEMMA FORALL (x:posreal):
%                      Integrable?[posreal](1,x,(LAMBDA (t: posreal): (1-t)^n/t))

%    ln_estimate_scaf3: LEMMA FORALL (x:posreal):
%                             ln(x) = Integral(1,x,LAMBDA (t:posreal): (1-t)^0/t)

   ln_estimate_scaf4: LEMMA x /= 1 IMPLIES
           1/(1-x) = sigma(0,n,(LAMBDA (i:nat): x^i)) + x^(n+1)/(1-x)

   ln_estimate_scaf5: LEMMA
           1/nzx = sigma(0,n,(LAMBDA (i:nat): (1-nzx)^i)) + (1-nzx)^(n+1)/nzx

%    ln_estimate_scaf6: LEMMA derivable[posreal](LAMBDA px: ln_estimate(px-1, n))

%    ln_estimate_scaf7: LEMMA deriv[posreal](LAMBDA px: ln_estimate(px-1, n+1))
%                 = (LAMBDA px: sigma(0,n,(LAMBDA (i:nat): (1-px)^i)))

%    ln_estimate_scaf8: LEMMA
%          ln(px) = ln_estimate(px-1,n+1) +
%                       Integral(1,px,LAMBDA (t:posreal): (1-t)^(n+1)/t)

%    ln_estimate_scaf9: LEMMA
%          ln(px) = ln_estimate(px-1,n) +
%                       Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t)

%    ln_estimate_scaf10: LEMMA 1 <= px AND px <= 2 IMPLIES
%            abs(Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t))
%                                         <= (px-1)^(n+1)/(n+1)

%    ln_estimate_scaf11: LEMMA px < 1 IMPLIES
%            abs(Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t))
%                                         <= (1-px)^(n+1)/((n+1)*px)

   ln_estimate_bnd: AXIOM abs(ln(1+z) - ln_estimate(z,n)) <=
                      abs(z)^(n+1)/(IF z < 0 THEN 1+z ELSE 1 ENDIF*(n+1))

   lnT(x:real_gtm1_le1)(n:nat):real_gtm1_le1 = -(-x)^(n+1)/(n+1)

%    lnT_convergence: LEMMA convergence(series(lnT(z)),ln(1+z))

%    lnT_convergent: LEMMA convergent(series(lnT(z)))

%    ln_series_def: LEMMA ln(1+z) = inf_sum(lnT(z))

   ln_taylors:     AXIOM EXISTS (c: between[{x:real | x > -1}](1,1+xgm1)):
                     ln(xgm1+1) = ln_estimate(xgm1,n) -(xgm1/-c)^(n+1)/(n+1)

%  Properties of exp

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

   expT(x)(n):real = IF n = 0 THEN 1 ELSE x^n / factorial(n) ENDIF

   exp_estimate(x,n):real = sigma(0,n,expT(x))

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

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

%    exp_series_scaf2: LEMMA sqrt(n)^(2*n) <= factorial(2*n)

%    exp_series_scaf3: LEMMA sqrt(n)^(2*n+1) <= factorial(2*n+1)

%    expT_convergence: LEMMA convergence(series(expT(x)),exp(x))

%    expT_convergent: LEMMA convergent(series(expT(x)))

%    exp_series: LEMMA exp(x) = inf_sum(expT(x))

END ln_exp_series_alt

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