Quelle ln_exp_series_alt.pvs Sprache: 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

quality84%

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