|
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.1 Sekunden
(vorverarbeitet)
¤
|
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.
|
