|
ln_approx: THEORY
%-----------------------------------------------------------------------------
% ln_approx by David Lester Manchester Univ
% Cesar Munoz NASA
% Anthony Narkawicz NASA
% ---------
% 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,ygt1: 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_ub_increasing: LEMMA
xgt1<=ygt1 IMPLIES
ln_gt1_ub(n,xgt1)<=ln_gt1_ub(n,ygt1)
ln_gt1_lb_increasing: LEMMA
xgt1<=ygt1 IMPLIES
ln_gt1_lb(n,xgt1)<=ln_gt1_lb(n,ygt1)
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_lb_increasing: LEMMA FORALL (px,py:posreal):
px <= py IMPLIES ln_lb(px,n) <= ln_lb(py,n)
ln_ub_increasing: LEMMA FORALL (px,py:posreal):
px <= py IMPLIES ln_ub(px,n) <= ln_ub(py,n)
ln_bounds: LEMMA ln_lb(px,n) <= ln(px) AND ln(px) <= ln_ub(px,n)
%%% Relationship of floor(ln(px)/ln(py)) to log_nat
floor_eq_log_nat_ge_1: LEMMA
FORALL ((xp:real|xp>=1),(np:posnat|np>1)):
floor(ln(xp)/ln(np)) = log_nat(xp,np)`1
END ln_approx
¤ Dauer der Verarbeitung: 0.30 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.
|
