Quellcode-Bibliothek ln_series.pvs Sprache: 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

quality94%

¤ 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.0.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.