|
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],
% convergence_special
IMPORTING reals@sigma_nat, reals@factorial, taylor_help
x: VAR real
n,m: VAR nat
a: VAR sequence[real]
l,t: VAR real
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: AXIOM 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)
END exp_series
¤ 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.
|
