|
exp_series: THEORY
%----------------------------------------------------------------------------
%
% Series expansion for Exponential 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[real], ints@factorial,
convergence_special,
reals@polynomials
x,y: VAR real
n,m: VAR nat
a: VAR sequence[real]
l,t: VAR real
AUTO_REWRITE+ sigma_0_neg
exp_seq(n): real = 1/factorial(n)
nderiv_exp: LEMMA derivable_n_times?(exp, n)
AND nderiv(n, exp) = exp
exp_inf_deriv: LEMMA inf_deriv_fun?[real](exp)
exp_series_prep: LEMMA
convergence(LAMBDA n: Taylor_rem(n,exp,0,x,
GET_C(exp,x,n)),0)
conv_exp: LEMMA conv_powerseries?[real](exp_seq)
exp_series: THEOREM exp = Inf_sum(exp_seq) % lim n->inf Sum x^n/n!
exp_estimate(x:real,n:nat):real =
1 + sigma(1,n,(LAMBDA (nn:nat): x^nn/factorial(nn)))
exp_taylors: LEMMA EXISTS (c: between[real](0,x)):
exp(x) = exp_estimate(x,n)
+ exp(c)*x^(n+1)/factorial(n+1)
exp_taylors_err: LEMMA abs(exp(x)-exp_estimate(x,n))
<= max(exp(x),1)*abs(x)^(n+1)/factorial(n+1)
exp_estimate_increasing: LEMMA
-1 <= x AND x<=y IMPLIES
exp_estimate(x,n) <= exp_estimate(y,n)
exp_estimate_positive: LEMMA
n>=2 AND -1 <= x IMPLIES
exp_estimate(x,n)>0
exp_estimate_0: LEMMA
exp_estimate(0,n) = 1
END exp_series
¤ Dauer der Verarbeitung: 0.15 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.
|
