|
%------------------------------------------------------------------------------
% exp
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
exp: THEORY
BEGIN
IMPORTING prelude_aux, cauchy, inv, int, shift, powerseries, log,
reals@factorial, lnexp_fnd@ln_exp, lnexp_fnd@ln_exp_series_alt,
lnexp_fnd@ln_approx
n,p: VAR nat
x: VAR real
cx: VAR cauchy_real
sx: VAR smallreal
csx: VAR cauchy_smallreal
cauchy_exp_series(n): cauchy_nnreal = cauchy_inv(cauchy_int(factorial(n)))
exp_series_lemma: LEMMA cauchy_prop(expT(1)(n), cauchy_exp_series(n))
exp_estimate_lemma:
LEMMA cauchy_prop(x,cx) =>
cauchy_prop(exp_estimate(x,n),
cauchy_powerseries(cx,cauchy_exp_series,n))
cauchy_exp_dr(csx)(p):int
= round(cauchy_powerseries(csx,cauchy_exp_series,p+3)(p+2)/4)
exp_dr_lemma: LEMMA cauchy_prop(sx,csx) =>
cauchy_prop(exp(sx),cauchy_exp_dr(csx))
JUDGEMENT cauchy_exp_dr(csx) HAS_TYPE cauchy_posreal
cauchy_exp(cx):[nat->int]
= LET n = cauchy_div(cx,cauchy_ln2)(0),
cy = cauchy_sub(cx,cauchy_mul(cauchy_int(n),cauchy_ln2))
IN IF n < 0 THEN cauchy_div2n(cauchy_exp_dr(cy),-n)
ELSIF n > 0 THEN cauchy_mul2n(cauchy_exp_dr(cy),n)
ELSE cauchy_exp_dr(cy) ENDIF
exp_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(exp(x),cauchy_exp(cx))
cauchy_exp_is_posreal: JUDGEMENT cauchy_exp(cx) HAS_TYPE cauchy_posreal
END exp
¤ Dauer der Verarbeitung: 0.20 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.
|
