|
ln_series: THEORY
%----------------------------------------------------------------------------
%
% Series Expansion for Natural Logarithm Function
%
% Author: Ricky W. Butler NASA Langley Research Center
%
% September 2012 by Anthony Narkawicz (Series is Increasing)
% Note. See ln_exp_series_alt for an alternate formulation
%----------------------------------------------------------------------------
BEGIN
IMPORTING ln_exp,
series@taylor_series,
convergence_special
x,y: VAR real
n,m: VAR nat
a: VAR sequence[real]
l,t: VAR real
abslt1: TYPE = {x: real | abs(x) < 1}
absle1: TYPE = {x: real | abs(x) <=1}
noa_posreal: LEMMA not_one_element?[posreal]
noa_gt_m1 : LEMMA not_one_element?[{x: real | x > -1}]
conn_gt_m1: LEMMA connected?[{x: real | x > -1}]
conn_posreal: LEMMA connected?[posreal]
conn_abslt1: LEMMA connected?[abslt1]
noa_abslt1: LEMMA not_one_element?[abslt1]
deriv_domain_gtm1: LEMMA deriv_domain?[{x: real | x > -1}]
AUTO_REWRITE+ noa_gt_m1
AUTO_REWRITE+ conn_gt_m1
AUTO_REWRITE+ noa_posreal
AUTO_REWRITE+ deriv_domain_posreal
AUTO_REWRITE+ conn_posreal
AUTO_REWRITE+ deriv_domain_gtm1
AUTO_REWRITE+ conn_abslt1
AUTO_REWRITE+ noa_abslt1
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
IMPORTING series@taylor_series[abslt1]
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: LEMMA EXISTS (c: between[{x:real | x > -1}](1,1+xgm1)):
ln(xgm1+1) = ln_estimate(xgm1,n) -(xgm1/-c)^(n+1)/(n+1)
ln_estimate_error_bound: LEMMA FORALL (xp:posreal):
abs(ln(xp+1)-ln_estimate(xp,n)) <= xp ^ (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,
reals@abs_lems,
analysis@integral_diff_doms
x1: VAR abslt1
lnp1: LEMMA ln(1+x1) = Integral(1,1+x1,(LAMBDA (t: posreal): 1/t))
ln_estimate_increasing_odd: LEMMA FORALL (px,py:real):
px<=py IMPLIES ln_estimate(px,2*n+1)<=ln_estimate(py,2*n+1)
ln_estimate_increasing_even: LEMMA FORALL (x1,y1:absle1):
x1<=y1 IMPLIES ln_estimate(x1,2*n)<=ln_estimate(y1,2*n)
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.21 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.
|
