exp_approx: THEORY %----------------------------------------------------------------------------- % Approximation of Exponential Function % ------------------------------------- % % Defines upper and lower bounds on exp: % - exp_lb(a,n) <= exp(a) <= exp_ub(a,n) % - e_lb(n) <= e <= e_ub(n) % % Author: David Lester Manchester University %-----------------------------------------------------------------------------
BEGIN
IMPORTING exp_series IMPORTING reals@quad_minmax % For proof only
n: VAR nat
pn: VAR posnat
x: VAR real
nx: VAR negreal
exp_neg_le1_ub(n,x): real = exp_estimate(x,2*n)
exp_neg_le1_lb(n,x): real = exp_estimate(x,2*n+1)
exp_neg_le1_bounds: LEMMA -1 <= x AND x < 0 IMPLIES
(exp_neg_le1_lb(n,x) < exp(x) AND exp(x) < exp_neg_le1_ub(n,x))
exp_neg_le1_ub_strict_decreasing_n: LEMMA -1 <= x AND x < 0 IMPLIES
strict_decreasing?(LAMBDA (n:nat): exp_neg_le1_ub(n,x))
exp_neg_le1_lb_strict_increasing_n: LEMMA -1 <= x AND x < 0 IMPLIES
strict_increasing?(LAMBDA (n:nat): exp_neg_le1_lb(n,x))
exp_neg_le1_lb_pos: LEMMA -1 <= x AND x < 0 IMPLIES exp_neg_le1_lb(pn,x) > 0
exp_neg_ub(n,nx):posreal = LET pn= -floor(nx) IN exp_neg_le1_ub(n+1,nx/pn)^pn
exp_neg_lb(n,nx):posreal = LET pn= -floor(nx) IN exp_neg_le1_lb(n+1,nx/pn)^pn
exp_ub(x,n): posreal = IF x < 0 THEN exp_neg_ub(n,x) ELSIF x = 0 THEN 1 ELSE 1/exp_neg_lb(n,-x) ENDIF
exp_lb(x,n): posreal = IF x < 0 THEN exp_neg_lb(n,x) ELSIF x = 0 THEN 1 ELSE 1/exp_neg_ub(n,-x) ENDIF
exp_bounds: LEMMA exp_lb(x,n) <= exp(x) AND exp(x) <= exp_ub(x,n)
e_lb(n) : posreal = exp_lb(1,n)
e_ub(n) : posreal = exp_ub(1,n)
e_bounds: LEMMA e_lb(n) <= e & e <= e_ub(n)
e_LB : MACRO posreal = 2718281828/1000000000
e_UB : MACRO posreal = 2718281829/1000000000
e_bounds2: LEMMA e_LB < e & e < e_UB
e_lb : posreal = 271/100
e_ub : posreal = 272/100
e_bound : JUDGEMENT e HAS_TYPE {x:posreal| e_lb < e AND e < e_ub}
END exp_approx
¤ 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.0.0Bemerkung:
(vorverarbeitet)
¤
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.
