|
trig_approx: THEORY
%-----------------------------------------------------------------------------
% trig_approx
% -----------
% - taylor series approximations to trig functions:
% sin_approx(a,n): sum first n terms of taylor expansion of sin
% cos_approx(a,n): sum first n terms of taylor expansion of cos
% - defines upper and lower bounds on trig functions:
%
% Version 2 Foundational (DRL) 4/4/05
%
% CHANGES
% - Redefined sin_lb,sin_ub,cos_lb,cos_ub,tan_lb,tan_ub to make it
% suitable for interval theory.
% - Removed lemmas SIN,COS,TAN. Use sin_bound_0_pi, cos_bound_npi2_pi2,
% tan_bound_0_pi2. Cesar Munoz (Nov 28 2003).
% - Added Hanne Gottliebsen's proofs for sin_bound_npi_0 and
% cos_bound_npi_pi.
% Cesar Munoz (Feb 6 2004).
% - Tan approximations moved to tan_approx due to circularity problems with
% trig_ineq. Cesar Munoz (Feb 6 2004)
% - The theory has been completely revisited by David Lester (4/4/05)
%
%-----------------------------------------------------------------------------
BEGIN
IMPORTING sincos, exp_term,
reals@factorial,
trig_ineq, reals@sigma_nat,
reals@real_fun_ops, reals@real_fun_preds
m,n: VAR nat
pm: VAR posnat
a: VAR real
px: VAR posreal
n0x: VAR nzreal
nnx: VAR nnreal
AUTO_REWRITE+ sigma_0_neg
sin_term(a)(n): real = (-1)^n*a^(2*n+1)/factorial(2*n+1)
sin_term_next : LEMMA sin_term(a)(n+1) =
sin_term(a)(n) * -1 * a*a / ((2*n+3)*(2*n+2))
sin_term_neg : LEMMA sin_term(-a)(n) = -sin_term(a)(n)
sin_terms_alternate : LEMMA 0 /= a IMPLIES (sin_term(a)(n+1) < 0 IFF
sin_term(a)(n) > 0)
sin_term_nonzero : LEMMA sin_term(a)(n) /= 0 IFF a /= 0
sin_term_zero : LEMMA sin_term(a)(n) = 0 IFF a = 0
sin_term_gt0 : LEMMA sin_term(a)(n) > 0 IFF
((even?(n) AND a > 0) OR (odd?(n) AND a < 0))
sin_term_lt0 : LEMMA sin_term(a)(n) < 0 IFF
((even?(n) AND a < 0) OR (odd?(n) AND a > 0))
sin_tends_to_0 : LEMMA tends_to_0?(sin_term(a))
cos_term(a)(n): real = IF n=0 THEN 1 ELSE (-1)^n*a^(2*n)/factorial(2*n) ENDIF
cos_term_next : LEMMA cos_term(a)(n+1) =
cos_term(a)(n) * -1 * a*a / ((2*n+2)*(2*n+1))
cos_term_neg : LEMMA cos_term(-a)(n) = cos_term(a)(n)
cos_terms_alternate : LEMMA 0 /= a IMPLIES (cos_term(a)(n+1) < 0 IFF
cos_term(a)(n) > 0)
cos_term_nonzero : LEMMA cos_term(a)(n) /= 0 IFF (n = 0 OR a /= 0)
cos_term_zero : LEMMA cos_term(a)(n) = 0 IFF (n /= 0 AND a = 0)
cos_term_gt0 : LEMMA cos_term(a)(n) > 0 IFF
(even?(n) AND (a /= 0 OR n = 0))
cos_term_lt0 : LEMMA cos_term(a)(n) < 0 IFF (odd?(n) AND a /= 0)
cos_tends_to_0 : LEMMA tends_to_0?(cos_term(n0x))
% sin_term_deriv: LEMMA derivable[real](LAMBDA a: sin_term(a)(n)) AND
% deriv[real](LAMBDA a: sin_term(a)(n)) = (LAMBDA a: cos_term(a)(n))
% cos_term_deriv: LEMMA derivable[real](LAMBDA a: cos_term(a)(n)) AND
% deriv[real](LAMBDA a: cos_term(a)(n)) =
% (LAMBDA a: IF n = 0 THEN 0 ELSE -sin_term(a)(n-1) ENDIF)
sin_approx(a,n):real = sigma(0,n,sin_term(a))
sin_approx_a0: LEMMA sin_approx(0,n) = 0
sin_approx_neg: LEMMA sin_approx(-a,n) = -sin_approx(a,n)
sin_approx_next: LEMMA sin_approx(a,n+2) - sin_approx(a,n) =
sin_term(a)(n+1) * (1 - a*a/((2*n+5)*(2*n+4)))
sin_approx_eq: LEMMA a*a = (2*n+5)*(2*n+4) IMPLIES
sin_approx(a,n+2) = sin_approx(a,n)
sin_approx_sin: LEMMA abs(sin(a)-sin_approx(a,n)) <= abs(sin_term(a)(n+1))
cos_approx(a,n):real = sigma(0,n,cos_term(a))
cos_approx_a0: LEMMA cos_approx(0,n) = 1
cos_approx_neg: LEMMA cos_approx(-a,n) = cos_approx(a,n)
cos_approx_cos: LEMMA abs(cos(a)-cos_approx(a,n)) <= abs(cos_term(a)(n+1))
cos_approx_next: LEMMA cos_approx(a,n+2) - cos_approx(a,n) =
cos_term(a)(n+1) * (1 - a*a/((2*n+4)*(2*n+3)))
cos_approx_eq: LEMMA a*a = (2*n+4)*(2*n+3) IMPLIES
cos_approx(a,n+2) = cos_approx(a,n)
% sin_approx_deriv: LEMMA derivable[real](LAMBDA a: sin_approx(a,n)) AND
% deriv[real](LAMBDA a: sin_approx(a,n))
% = (LAMBDA a: cos_approx(a,n))
% cos_approx_deriv: LEMMA derivable[real](LAMBDA a: cos_approx(a,n)) AND
% deriv[real](LAMBDA a: cos_approx(a,n)) =
% (LAMBDA a: IF n = 0 THEN 0 ELSE -sin_approx(a,n-1) ENDIF)
sin_ub(a,n):real = IF a < 0 THEN sin_approx(a,2*n+1)
ELSE sin_approx(a,2*n) ENDIF
sin_lb(a,n):real = IF a < 0 THEN sin_approx(a,2*n)
ELSE sin_approx(a,2*n+1) ENDIF
sin_lb_neg: LEMMA sin_lb(-a,n) = -sin_ub(a,n)
sin_ub_neg: LEMMA sin_ub(-a,n) = -sin_lb(a,n)
sin_lb_a0 : LEMMA sin_lb(0,n) = 0
sin_ub_a0 : LEMMA sin_ub(0,n) = 0
sin_lb_ub : LEMMA sin_lb(n0x,n) < sin_ub(n0x,n)
sin_lb_inc: LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin_lb(px,n+pm)
sin_ub_dec: LEMMA px*px < (4*n+5)*(4*n+4) => sin_ub(px,n+pm) < sin_ub(px,n)
sin_lb_lt : LEMMA px*px < (4*n+7)*(4*n+6) => sin_lb(px,n) < sin(px)
sin_ub_lt : LEMMA px*px < (4*n+5)*(4*n+4) => sin(px) < sin_ub(px,n)
sin_lb_gt : LEMMA px*px > (4*n+7)*(4*n+6) => sin_lb(px,n) < -1
sin_ub_gt : LEMMA px*px > (4*n+5)*(4*n+4) => sin_ub(px,n) > 1
sin_lb : LEMMA sin_lb(n0x,n) < sin(n0x)
sin_ub : LEMMA sin(n0x) < sin_ub(n0x,n)
sin_bounds : LEMMA sin_lb(a,n) <= sin(a) AND sin(a) <= sin_ub(a,n)
sin_lb_gt0: LEMMA px*px < 6 => sin_lb(px,n) > 0
cos_ub(a,n):real = cos_approx(a,2*n)
cos_lb(a,n):real = cos_approx(a,2*n+1)
cos_lb_neg: LEMMA cos_lb(-a,n) = cos_lb(a,n)
cos_ub_neg: LEMMA cos_ub(-a,n) = cos_ub(a,n)
cos_lb_a0 : LEMMA cos_lb(0,n) = 1
cos_ub_a0 : LEMMA cos_ub(0,n) = 1
cos_lb_ub: LEMMA cos_lb(n0x,n) < cos_ub(n0x,n)
cos_lb_inc: LEMMA n0x*n0x<(4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos_lb(n0x,n+pm)
cos_ub_dec: LEMMA n0x*n0x<(4*n+4)*(4*n+3) => cos_ub(n0x,n+pm) < cos_ub(n0x,n)
cos_lb_lt: LEMMA n0x*n0x < (4*n+6)*(4*n+5) => cos_lb(n0x,n) < cos(n0x)
cos_ub_lt: LEMMA n0x*n0x < (4*n+4)*(4*n+3) => cos(n0x) < cos_ub(n0x,n)
cos_lb_gt: LEMMA n0x*n0x > (4*n+6)*(4*n+5) => cos_lb(n0x,n) < -1
cos_ub_gt: LEMMA n0x*n0x > (4*n+4)*(4*n+3) & n>=1 => cos_ub(n0x,n) > 1
cos_lb: LEMMA cos_lb(n0x,n) < cos(n0x)
cos_ub: LEMMA cos(n0x) < cos_ub(n0x,pm)
cos_bounds: LEMMA cos_lb(a,n) <= cos(a) AND cos(a) <= cos_ub(a,n)
% sin_lb_deriv: LEMMA derivable[nnreal](LAMBDA nnx: sin_lb(nnx,n)) AND
% deriv[nnreal](LAMBDA nnx: sin_lb(nnx,n)) = (LAMBDA nnx: cos_lb(nnx,n))
% sin_ub_deriv: LEMMA derivable[nnreal](LAMBDA nnx: sin_ub(nnx,n)) AND
% deriv[nnreal](LAMBDA nnx: sin_ub(nnx,n)) = (LAMBDA nnx: cos_ub(nnx,n))
% cos_lb_deriv: LEMMA derivable[real](LAMBDA a: cos_lb(a,n)) AND
% deriv[real](LAMBDA a: cos_lb(a,n))
% = (LAMBDA a: IF a < 0 THEN -sin_lb(a,n) ELSE -sin_ub(a,n) ENDIF)
% cos_ub_deriv: LEMMA derivable[real](LAMBDA a: cos_ub(a,n)) AND
% deriv[real](LAMBDA a: cos_ub(a,n))
% = (LAMBDA a: IF n = 0 THEN 0 ELSIF
% a < 0 THEN -sin_ub(a,n-1) ELSE -sin_lb(a,n-1) ENDIF)
cos_lb_nn_strict_decreasing: AXIOM
strict_decreasing?(LAMBDA (x:{x:nnreal| x <= pi}): cos_lb(x,n))
cos_lb_np_strict_increasing: LEMMA
strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi}): cos_lb(x,n))
%
% ---- Added 1/8/2008
%
sin_px: LEMMA 1/500 > px => sin(px) > px*(1-1/1500000)
% Approximation to guarantee cos_lb > 0
IMPORTING atan_approx
Cos_pos_n : MACRO posnat = 5
cos_term_pi_lb: LEMMA n >= Cos_pos_n IMPLIES
cos_term(pi_lbn(n)/2)(2*n+2) < cos(pi_lbn(n)/2)
cos_lb_pi2_eps: LEMMA px <= pi/2 AND
abs(cos_term(pi/2-px)(2*n+2)) < sin(px) =>
cos_lb(pi/2-px,n) > 0
cos_lb_pi2_pos0 : LEMMA n=0 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos1 : LEMMA n=1 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos2 : LEMMA n=2 => NOT cos_lb(pi_lbn(n)/2,n) > 0
cos_lb_pi2_pos : LEMMA
n >= Cos_pos_n IMPLIES
cos_lb(pi_lbn(n)/2,n) > 0
END trig_approx
¤ Dauer der Verarbeitung: 0.15 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.
|
