|
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_neg_bounds: LEMMA exp_neg_lb(n,nx) < exp(nx) & exp(nx) < exp_neg_ub(n,nx)
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
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
