|
%------------------------------------------------------------------------------
% Power
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
power: THEORY
BEGIN
IMPORTING prelude_aux, prelude_A4, appendix, cauchy, unique
w,x,y,z,a,b: VAR real
pn,q0,q1: VAR posnat
p,q,p1,n: VAR nat
cx: VAR cauchy_real
scx: VAR cauchy_smallreal
sx: VAR smallreal
r,X,Y,X0: VAR int
rx: VAR rat
e1: VAR posreal
abs_ge0: LEMMA 0 <= abs(x)
abs_neg: LEMMA abs(-x) = abs(x)
abs_interval: LEMMA abs(x-y) < a <=> x-a < y AND y < x+a
abs_interval1: LEMMA abs(x) < a <=> -a < x AND x < a
abs_interval2: LEMMA abs(x) <= a <=> -a <= x AND x <= a
triangle_open: LEMMA abs(x-y) < a AND abs(y-z) < b => abs(x-z) < a+b
abs_error: LEMMA abs(x-y) < a AND abs(w-z) < b => abs(x+w-(y+z)) < a+b
lemma_A2_generalized: LEMMA r = round(x) => r-1/2 <= x AND x < r+1/2
cauchy_power_lt1_n_odd: LEMMA
odd?(pn) AND sx+e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_n_even: LEMMA
even?(pn) AND sx+e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_snz_odd: LEMMA
odd?(pn) AND sx < 0 AND sx+e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_snz_even: LEMMA
even?(pn) AND sx < 0 AND sx+e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_sn_odd: LEMMA
odd?(pn) AND sx < 0 AND 0 < sx+e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_sn_even: LEMMA
even?(pn) AND sx < 0 AND 0 < sx+e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_z: LEMMA
sx = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_sp_odd: LEMMA
odd?(pn) AND 0 < sx AND sx-e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_sp_even: LEMMA
even?(pn) AND 0 < sx AND sx-e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_pz: LEMMA
sx-e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_p: LEMMA
0 < sx-e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_main_generalized: LEMMA
Y = round ((rx*2^-(p+floor(log2(pn))+3))^pn*2^p) AND
rx-1 < sx * 2^(p+floor(log2(pn))+3) AND
sx * 2^(p+floor(log2(pn))+3) < rx+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_main: LEMMA
Y = round ((X*2^-(p+floor(log2(pn))+3))^pn*2^p) AND
X-1 < sx * 2^(p+floor(log2(pn))+3) AND
sx * 2^(p+floor(log2(pn))+3) < X+1 =>
Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y
cauchy_power_lt1_isreal: LEMMA cauchy_real?
(LAMBDA p: round ((scx(p+floor(log2(pn))+3) *
2^-(p+floor(log2(pn))+3))^pn*2^p))
cauchy_power_lt1(scx:cauchy_smallreal, pn:posnat):cauchy_real
= (LAMBDA p: round ((scx(p+floor(log2(pn))+3) *
2^-(p+floor(log2(pn))+3))^pn*2^p))
power_lemma_lt1: LEMMA cauchy_prop(sx,scx)
=> cauchy_prop(sx^pn, cauchy_power_lt1(scx,pn))
cauchy_power_div1: LEMMA X0-1 < x AND x < X0+1 AND
p = floor(log2(abs(X0)+1))+1 =>
-(2^p) < x AND x < 2^p
cauchy_power_main: LEMMA
X0-1 < x AND x < X0+1 AND q = 1+floor(log2(abs(X0)+1)) AND
p1 = p+floor(log2(pn))+3+pn*q AND Y = round ((X/2^p1)^pn*2^p) AND
X-1 < x * 2^p1 AND x * 2^p1 < X+1 =>
Y-1 < x^pn * 2^p AND x^pn * 2^p < 1+Y
cauchy_power_isreal: LEMMA cauchy_real?
(LAMBDA p:
LET p1 = p+floor_log2(pn)+3+pn*(1+floor_log2(abs(cx(0))+1))
IN round((cx(p1)*2^-(p1))^pn*2^p))
cauchy_power(cx:cauchy_real, pn:posnat):cauchy_real
= (LAMBDA p: LET p1 = p+floor_log2(pn)+3+pn*(1+floor_log2(abs(cx(0))+1))
IN round((cx(p1)*2^-(p1))^pn*2^p))
power_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(x^pn,cauchy_power(cx,pn))
END power
¤ Dauer der Verarbeitung: 0.2 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.
|
