Quelle  ln_exp_series_alt.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,
             analysis@nth_derivatives, analysis@taylors, series@series,
             analysis@integral, analysis@indefinite_integral, reals@sqrt

   noa_posreal      : LEMMA not_one_element?[posreal]
   conn_posreal     : LEMMA connected?[posreal]
   noa_gt_m1        : LEMMA not_one_element?[{x: real | x > -1}]
   conn_gt_m1       : LEMMA connected?[{x: real | x > -1}]
   deriv_domain_gtm1: LEMMA deriv_domain?[{x: real | x > -1}]

   AUTO_REWRITE+ noa_gt_m1 
   AUTO_REWRITE+ conn_gt_m1
   AUTO_REWRITE+ deriv_domain_gtm1
   AUTO_REWRITE+ noa_posreal
   AUTO_REWRITE+ conn_posreal
   AUTO_REWRITE+ deriv_domain_posreal


   AUTO_REWRITE+ sigma_0_neg

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