|
atan_approx: THEORY
%-----------------------------------------------------------------------------
% atan_approx by David Lester
% -----------
% Defines upper and lower bounds on atan and pi:
% - atan_lb(a,n) <= atan(a) <= atan_ub(a,n)
% - pi_lb(a,n) <= pi <= pi_ub(n)
%
% Additions 2012 by Anthony Narkawicz
%
%-----------------------------------------------------------------------------
BEGIN
IMPORTING atan,sincos_def
m,n : VAR nat
x : VAR real
px,py : VAR posreal
atan_pos_le1_ub(n,x): real = atan_series_n(x,2*n)
atan_pos_le1_lb(n,x): real = atan_series_n(x,2*n+1)
atan_pos_le1_ub_lt : LEMMA
0 < x AND x <= 1 IMPLIES
atan_pos_le1_ub(n+1,x) < atan_pos_le1_ub(n,x)
atan_pos_le1_lb_lt : LEMMA
0 < x AND x <= 1 IMPLIES
atan_pos_le1_lb(n,x) < atan_pos_le1_lb(n+1,x)
atan_pos_le1_bounds: LEMMA 0 < x AND x <= 1 IMPLIES
(atan_pos_le1_lb(n,x) < atan(x) AND atan(x) < atan_pos_le1_ub(n,x))
atan_pos_le1_lb_inc: LEMMA px <= 1 AND n < m =>
atan_pos_le1_lb(n,px) < atan_pos_le1_lb(m,px)
atan_pos_le1_ub_dec: LEMMA px <= 1 AND n < m =>
atan_pos_le1_ub(m,px) < atan_pos_le1_ub(n,px)
pi_lbn(n): real = 4*(4*atan_pos_le1_lb(n,1/5) - atan_pos_le1_ub(n,1/239))
pi_ubn(n): real = 4*(4*atan_pos_le1_ub(n,1/5) - atan_pos_le1_lb(n,1/239))
pi_lbn_lt : LEMMA
pi_lbn(n) < pi_lbn(n+1)
pi_lbn_LT : LEMMA
FORALL (k:above(n)):
pi_lbn(n) < pi_lbn(k)
pi_bounds: LEMMA pi_lbn(n) < pi AND pi < pi_ubn(n)
pi_lb_pos : JUDGEMENT
pi_lbn(n) HAS_TYPE posreal
pi_ub_pos : JUDGEMENT
pi_ubn(n) HAS_TYPE posreal
pi_bounds0: LEMMA pi_lbn(0) = 281476/89625 AND % > 3.1405
pi_ubn(0) = 651864872/204778785 % < 3.1837
pi_lb : posreal = 31415926/10000000
pi_ub : posreal = 31415927/10000000
pi_bounds2: LEMMA pi_lb < pi_lbn(2) AND pi_ubn(2) < pi_ub
pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb < r AND r < pi_ub}
pi_lb_inc: LEMMA n < m => pi_lbn(n) < pi_lbn(m)
pi_ub_dec: LEMMA n < m => pi_ubn(m) < pi_ubn(n)
atan_pos_lb(n,px): real = IF px <= 1 THEN atan_pos_le1_lb(n,px) ELSE
max(atan_pos_le1_lb(n,1),pi_lbn(n)/2 - atan_pos_le1_ub(n,1/px)) ENDIF
atan_pos_ub(n,px): real = IF px <= 1 THEN atan_pos_le1_ub(n,px) ELSE
max(atan_pos_le1_ub(n,1),pi_ubn(n)/2 - atan_pos_le1_lb(n,1/px)) ENDIF
atan_pos_bounds: LEMMA 0 < x IMPLIES
(atan_pos_lb(n,x) < atan(x) AND atan(x) < atan_pos_ub(n,x))
atan_lb(x,n): real = IF x > 0 THEN atan_pos_lb(n,x)
ELSIF x = 0 THEN 0
ELSE -atan_pos_ub(n,-x) ENDIF
atan_ub(x,n): real = IF x > 0 THEN atan_pos_ub(n,x)
ELSIF x = 0 THEN 0
ELSE -atan_pos_lb(n,-x) ENDIF
atan_bounds: LEMMA atan_lb(x,n) <= atan(x) AND atan(x) <= atan_ub(x,n)
atan_lb_increasing: LEMMA increasing?(LAMBDA (x:real): atan_lb(x,n))
atan_ub_increasing: LEMMA increasing?(LAMBDA (x:real): atan_ub(x,n))
atan_pos_lb_inc: LEMMA n <= m => atan_pos_lb(n,px) <= atan_pos_lb(m,px)
atan_pos_ub_dec: LEMMA n <= m => atan_pos_ub(m,px) <= atan_pos_ub(n,px)
pi_lb_pi: LEMMA pi-pi_lbn(n) <= 16*((1/5)^(4*n+5)/(4*n+5)) +
4*((1/239)^(4*n+3)/(4*n+3))
pi_ub_pi: LEMMA pi_ubn(n)-pi <= 16*((1/5)^(4*n+3)/(4*n+3)) +
4*((1/239)^(4*n+5)/(4*n+5))
pi_lb_diff: LEMMA pi_lbn(n+1)-pi_lbn(n) =
16*(1/5)^(4*n+5)*(1/(4*n+5) - 1/(25*(4*n+7))) +
4*(1/239)^(4*n+3)*(1/(4*n+3) - 1/(57121*(4*n+5)))
pi_ub_diff: LEMMA pi_ubn(n)-pi_ubn(n+1) =
16*(((1/5)^(3+4*n))*(1/(3+4*n)))
-16*(((1/5)^(5+4*n))*(1/(5+4*n)))
+4*(((1/239)^(5+4*n))*(1/(5+4*n)))
-4*(((1/239)^(7+4*n))*(1/(7+4*n)))
pi_lb_diff_bounds: LEMMA n>=5 IMPLIES
LET xdiff = pi_lbn(n+1)-pi_lbn(n) IN
14*(1/5)^(5*n+5) < xdiff AND xdiff < (116/25)*(1/5)^(4*n+3)
pi_lb_quot_bounds: LEMMA
LET xquot = pi_lbn(n)/pi_lbn(n+1) IN
1-14.5*(1/5)^(4*n+3) <= xquot AND xquot <= 1
pi_ub_diff_bounds: LEMMA n>=5 IMPLIES
LET xdiff = pi_ubn(n)-pi_ubn(n+1) IN
32*(1/5)^(5*n+3) < xdiff AND xdiff < (7/5)*(1/5)^(4*n+3)
pi_ub_quot_bounds: LEMMA
LET xquot = pi_ubn(n+1)/pi_ubn(n) IN
1-(9/5)*(1/5)^(4*n+3) <= xquot AND xquot <= 1
END atan_approx
¤ 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.
|
