|
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,
% series@nth_derivatives, series@taylors, series@series,
% analysis@integral,
reals@sqrt, reals@sigma_nat, reals@factorial, taylor_help
% 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: AXIOM 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: AXIOM 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: AXIOM 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.14 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.
|
