|
%------------------------------------------------------------------------------
% Arctangent
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
atanx: THEORY
BEGIN
IMPORTING prelude_aux, sqrtx, int, add, sub, mul, div, shift, cauchy,
sum, power, powerseries, trig_fnd@atan
p: VAR nat
ssmallreal: NONEMPTY_TYPE = {x:real | -1/2 < x & x < 1/2} CONTAINING 0
cauchy_ssmallreal?(c:[nat->int]):bool=EXISTS (x:ssmallreal): cauchy_prop(x,c)
cauchy_ssmallreal: NONEMPTY_TYPE=(cauchy_ssmallreal?) CONTAINING (LAMBDA p:0)
JUDGEMENT cauchy_ssmallreal SUBTYPE_OF cauchy_real
vsmallreal: NONEMPTY_TYPE = {x:real | 0 <= x & x < 1/4} CONTAINING 0
cauchy_vsmallreal?(c:[nat->int]):bool=EXISTS (x:vsmallreal):cauchy_prop(x,c)
cauchy_vsmallreal:NONEMPTY_TYPE=(cauchy_vsmallreal?) CONTAINING (LAMBDA p:0)
JUDGEMENT cauchy_vsmallreal SUBTYPE_OF cauchy_real
x: VAR real
cx: VAR cauchy_real
ssx: VAR ssmallreal
cssx: VAR cauchy_ssmallreal
n: VAR nat
vsx: VAR vsmallreal
cvsx: VAR cauchy_vsmallreal
cauchy_atan_drx_series(n:nat): cauchy_real
= (IF even?(n) THEN cauchy_div(cauchy_int( 1),cauchy_int(2*n+1))
ELSE cauchy_div(cauchy_int(-1),cauchy_int(2*n+1)) ENDIF)
atan_series_lemma:
LEMMA cauchy_prop(atan_series_coef(n), cauchy_atan_drx_series(n))
cauchy_atan_drxx(cvsx:cauchy_vsmallreal): [nat->int]
= (LAMBDA p:
round(cauchy_powerseries(cvsx,cauchy_atan_drx_series,p+2)(p+2)/4))
cauchy_atan_drxx_prop: LEMMA cauchy_prop(vsx,cvsx) =>
cauchy_prop(IF vsx = 0 THEN 1 ELSE atan(sqrt(vsx))/sqrt(vsx) ENDIF,
cauchy_atan_drxx(cvsx))
cauchy_atan_dr(cssx:cauchy_ssmallreal): cauchy_real
= cauchy_mul(cssx,cauchy_atan_drxx(cauchy_mul(cssx,cssx)))
atan_dr_lemma: LEMMA cauchy_prop(ssx,cssx) =>
cauchy_prop(atan(ssx),cauchy_atan_dr(cssx))
cauchy_pi: cauchy_real
= cauchy_sub(cauchy_mul2n(cauchy_atan_dr(cauchy_div(cauchy_int(1),
cauchy_int(5))),4),
cauchy_mul2n(cauchy_atan_dr(cauchy_div(cauchy_int(1),
cauchy_int(239))),2))
pi_lemma: LEMMA cauchy_prop(pi,cauchy_pi)
% |x-cx(3)| < 1/8 IMPLIES
% (-4) <= t <= -3 => -1/2 < x < -1/4 =>
% -2 <= t <= 2 => -3/8 < x < 3/8
% 3 <= t <= (4) => 1/4 < x < 1/2 =>
% cauchy_atan_dr(csx:cauchy_real): cauchy_real
% = LET t = csx(3),
% p6 = cauchy_div(cauchy_pi,cauchy_int(6)),
% s3 = cauchy_sqrt(cauchy_int(3)),
% n = cauchy_div(cauchy_add(cauchy_mul(csx,s3), cauchy_int(1)),
% cauchy_sub(s3,csx)),
% p = cauchy_div(cauchy_sub(cauchy_mul(csx,s3), cauchy_int(1)),
% cauchy_add(s3,csx))
% IN IF t < -4 THEN cauchy_sub(cauchy_atan_drx(n),p6)
% ELSIF t < 5 THEN cauchy_atan_drx(csx)
% ELSE cauchy_add(cauchy_atan_drx(p),p6)
% ENDIF
% Was |x-cx(2)| < 1/4 IMPLIES
% t <= -5 => x < -1 => 0 < -1/x < 1
% t = -4 => -5/4 < x < -3/4 => -1/7 < x+1/x-1 < 1/9
% -3 <= t <= 3 => -1 < x < 1
% t = 4 => 3/4 < x < 5/4 => -1/7 < x-1/x+1 < 1/9
% 5 <= t => 1 < x => 0 < 1/x < 1
% |x-cx(3)| < 1/8 IMPLIES
% t <= -20 => x < -19/8 => 0 < -1/x < 8/19
% -19 <= t <= -4 => -5/2 < x < -3/8 => -5/11 < x+1/x-1 < 3/7
% -3 <= t <= 3 => -1/2 < x < 1/2
% 4 <= t <= 19 => 3/8 < x < 5/2 => -5/11 < x-1/x+1 < 3/7
% 20 <= t => 19/8 < x => 0 < 1/x < 8/19
cauchy_atan(cx:cauchy_real): cauchy_real
= LET t = cx(3),
cxm1 = cauchy_sub(cx,cauchy_int(1)),
cxp1 = cauchy_add(cx,cauchy_int(1)),
p2 = cauchy_div2n(cauchy_pi,1),
p4 = cauchy_div2n(cauchy_pi,2)
IN IF t <= -20 THEN cauchy_sub(
cauchy_atan_dr(cauchy_neg(cauchy_inv(cx))),
p2)
ELSIF t <= -4 THEN cauchy_sub(cauchy_neg(p4),
cauchy_atan_dr(cauchy_div(cxp1,cxm1)))
ELSIF t <= 3 THEN cauchy_atan_dr(cx)
ELSIF t <= 19 THEN cauchy_add(p4,
cauchy_atan_dr(cauchy_div(cxm1,cxp1)))
ELSE cauchy_sub(p2, cauchy_atan_dr(cauchy_inv(cx)))
ENDIF
atan_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(atan(x),cauchy_atan(cx))
END atanx
¤ Dauer der Verarbeitung: 0.1 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.
|
