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
