Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: axiomatic.pvs Sprache: PVS

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.