| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lnexp_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle ln_series.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28