|
ln_exp_series_alt: THEORY
%------------------------------------------------------------------------------
%
% Alternate means of establishing infinite series for ln and exp
%
% Author: David Lester
%
%
%------------------------------------------------------------------------------
BEGIN
real_gtm1_le1: NONEMPTY_TYPE = {x:real | -1 < x AND x <= 1} CONTAINING 0
x: VAR real
px: VAR posreal
xgm1: VAR {x:real | x > -1}
nzx: VAR nzreal
z: VAR real_gtm1_le1
n: VAR nat
IMPORTING ln_exp, analysis@derivative_inverse,
analysis@nth_derivatives, analysis@taylors, series@series,
analysis@integral, analysis@indefinite_integral, reals@sqrt
noa_posreal : LEMMA not_one_element?[posreal]
conn_posreal : LEMMA connected?[posreal]
noa_gt_m1 : LEMMA not_one_element?[{x: real | x > -1}]
conn_gt_m1 : LEMMA connected?[{x: real | x > -1}]
deriv_domain_gtm1: LEMMA deriv_domain?[{x: real | x > -1}]
AUTO_REWRITE+ noa_gt_m1
AUTO_REWRITE+ conn_gt_m1
AUTO_REWRITE+ deriv_domain_gtm1
AUTO_REWRITE+ noa_posreal
AUTO_REWRITE+ conn_posreal
AUTO_REWRITE+ deriv_domain_posreal
AUTO_REWRITE+ sigma_0_neg
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
ln_estimate(x:real,n:nat):real
= sigma(0,n,(LAMBDA (nn:nat): IF nn=0 THEN 0 ELSE -(-x)^nn/nn ENDIF))
ln_estimate_scaf1: LEMMA continuous?((LAMBDA (t: posreal): (1-t)^n/t))
ln_estimate_scaf2: LEMMA FORALL (x:posreal):
Integrable?[posreal](1,x,(LAMBDA (t: posreal): (1-t)^n/t))
ln_estimate_scaf3: LEMMA FORALL (x:posreal):
ln(x) = Integral(1,x,LAMBDA (t:posreal): (1-t)^0/t)
ln_estimate_scaf4: LEMMA x /= 1 IMPLIES
1/(1-x) = sigma(0,n,(LAMBDA (i:nat): x^i)) + x^(n+1)/(1-x)
ln_estimate_scaf5: LEMMA
1/nzx = sigma(0,n,(LAMBDA (i:nat): (1-nzx)^i)) + (1-nzx)^(n+1)/nzx
ln_estimate_scaf6: LEMMA derivable?[posreal](LAMBDA px: ln_estimate(px-1, n))
ln_estimate_scaf7: LEMMA deriv[posreal](LAMBDA px: ln_estimate(px-1, n+1))
= (LAMBDA px: sigma(0,n,(LAMBDA (i:nat): (1-px)^i)))
ln_estimate_scaf8: LEMMA
ln(px) = ln_estimate(px-1,n+1) +
Integral(1,px,LAMBDA (t:posreal): (1-t)^(n+1)/t)
ln_estimate_scaf9: LEMMA
ln(px) = ln_estimate(px-1,n) +
Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t)
ln_estimate_scaf10: LEMMA 1 <= px AND px <= 2 IMPLIES
abs(Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t))
<= (px-1)^(n+1)/(n+1)
ln_estimate_scaf11: LEMMA px < 1 IMPLIES
abs(Integral(1,px,LAMBDA (t:posreal): (1-t)^n/t))
<= (1-px)^(n+1)/((n+1)*px)
ln_estimate_bnd: LEMMA abs(ln(1+z) - ln_estimate(z,n)) <=
abs(z)^(n+1)/(IF z < 0 THEN 1+z ELSE 1 ENDIF*(n+1))
lnT(x:real_gtm1_le1)(n:nat):real_gtm1_le1 = -(-x)^(n+1)/(n+1)
lnT_convergence: LEMMA convergence(series(lnT(z)),ln(1+z))
lnT_convergent: LEMMA convergent?(series(lnT(z)))
ln_series_def: LEMMA ln(1+z) = inf_sum(lnT(z))
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)
% Properties of exp
nderiv_exp: LEMMA derivable_n_times?(exp, n)
AND nderiv(n, exp) = exp
expT(x)(n):real = IF n = 0 THEN 1 ELSE x^n / factorial(n) ENDIF
exp_estimate(x,n):real = sigma(0,n,expT(x))
exp_taylors: LEMMA EXISTS (c:between[real](0,x)):
exp(x) = exp_estimate(x,n) + exp(c)*x^(n+1)/factorial(n+1)
exp_estimate_bnd: LEMMA abs(exp(x)-exp_estimate(x,n))
<= max(exp(x),1)*abs(x)^(n+1)/factorial(n+1)
exp_series_scaf2: LEMMA sqrt(n)^(2*n) <= factorial(2*n)
exp_series_scaf3: LEMMA sqrt(n)^(2*n+1) <= factorial(2*n+1)
expT_convergence: LEMMA convergence(series(expT(x)),exp(x))
expT_convergent: LEMMA convergent?(series(expT(x)))
exp_series: LEMMA exp(x) = inf_sum(expT(x))
END ln_exp_series_alt
¤ Dauer der Verarbeitung: 0.16 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.
|
