|
ln_approx: THEORY
%-----------------------------------------------------------------------------
% ln_approx by David Lester Manchester Univ
% Cesar Munoz NIA
% ---------
% Defines upper and lower bounds on ln:
% - ln_lb(a,n) <= ln(a) <= ln_ub(a,n)
%-----------------------------------------------------------------------------
BEGIN
IMPORTING ln_series,reals@log_nat
n: VAR nat
x: VAR real
px: VAR posreal
pn: VAR posnat
xgt1: VAR {x:posreal | x > 1}
ln_le2_lb(n,x): real = if x = 0 then 0 else ln_estimate(x,2*n) endif
ln_le2_ub(n,x): real = if x = 0 then 0 else ln_estimate(x,2*n+1) endif
ln_le2_bounds: LEMMA 0 < x AND x <= 1 IMPLIES
(ln_le2_lb(n,x) < ln(x+1) AND ln(x+1) < ln_le2_ub(n,x))
ln2_lb(n): MACRO real = ln_le2_lb(n,1)
ln2_ub(n): MACRO real = ln_le2_ub(n,1)
ln_gt1_lb(n,xgt1): real =
let (m,y) = log_nat(xgt1,2) in
m*ln2_lb(n)+ln_le2_lb(n,y-1)
ln_gt1_ub(n,xgt1): real =
let (m,y) = log_nat(xgt1,2) in
m*ln2_ub(n)+ln_le2_ub(n,y-1)
ln_gt1_bounds: LEMMA 1 < x IMPLIES
(ln_gt1_lb(n,x) < ln(x) AND ln(x) < ln_gt1_ub(n,x))
ln_lb(px,n): real = IF px < 1 THEN -ln_gt1_ub(n,1/px)
ELSIF px = 1 THEN 0
ELSE ln_gt1_lb(n,px) ENDIF
ln_ub(px,n): real = IF px < 1 THEN -ln_gt1_lb(n,1/px)
ELSIF px = 1 THEN 0
ELSE ln_gt1_ub(n,px) ENDIF
ln_bounds: LEMMA ln_lb(px,n) <= ln(px) AND ln(px) <= ln_ub(px,n)
END ln_approx
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
