Quelle  ln_series.pvs   Sprache: unbekannt

ln_series: THEORY
%----------------------------------------------------------------------------
%
%  Series Expansion for Natural Logarithm 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, 
%              convergence_special

   IMPORTING reals@sigma_nat

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


%    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


   abslt1: TYPE = {x: real | abs(x) < 1}


%   IMPORTING series@taylor_series[abslt1] 

   IMPORTING taylor_help

   Gt_m1: TYPE = {x:real | x > -1}
   xgm1:  VAR Gt_m1

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

   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)

%   --- Series for log(1+x) follows from term-by-term integration
%   --- of 1/(1+x) = 1 - x + x^2 - x^3.  Using term-by-term
%   --- in power_series_integ, we can use proof in Rosenlicht
%   --- page 155 or Salas-Hille pg 466 to get log(1+x) series for abs(x) < 1
%   --- Also use corollary 3 on pg 128 of Rosenlicht to establish that
%   --- ln(1+x) = integral(1,1+x,1/t) = integral(0,x,1/(1+t))
%

%   IMPORTING analysis@integral_chg_var,
%             analysis@abs_props,
%             analysis@integral_diff_doms


   x1: VAR abslt1

%    lnp1: LEMMA ln(1+x1) = Integral(1,1+x1,(LAMBDA (t: posreal): 1/t)) 


%    lnp1_prep: LEMMA  Integrable?(0,x1,(LAMBDA (u: Gt_m1): 1/(u+1))) AND
%                        Integral(1,1+x1,(LAMBDA (t: posreal): 1/t)) = 
%                        Integral(0,x1,(LAMBDA (u: Gt_m1): 1/(u+1)))


%     geom_neg: LEMMA abs(x) < 1 IMPLIES 
%                                convergent(series(LAMBDA n: (-x) ^ n))  AND
%                                1/(1+x) = inf_sum((LAMBDA n: (-x)^n))

    lnp1(x: abslt1): real = ln(1+x)

    lnp1_seq(n): real = IF n = 0 THEN 0 ELSE (-1)^(n+1)/n ENDIF


%    IMPORTING series@power_series_integ

%    lnp1_conv: LEMMA conv_powerseries?[abslt1](lnp1_seq)

%    int_geo_prep: LEMMA Integrable?(0,x1,(LAMBDA (u: abslt1): 1 / (1 + u)))

%   ----- ln(1 + x) = x - x^2/2 + x^3/3 - x^4/4 + .... if |x| < 1 -----

%   int_geo_neg: LEMMA conv_powerseries?[abslt1](lnp1_seq) AND
%                      Integral(0,x1,(LAMBDA (u: {x:real | x > -1}): 1/(u+1))) 
%                          = Inf_sum(lnp1_seq)(x1)  % inf Sum - (-1)^n/n x^n


END ln_series

quality94%

[ zur Elbe Produktseite wechseln0.13Quellennavigators  Analyse erneut starten  ]