| products/Sources/formale Sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_approx.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
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. Cear Munoz (Feb 6 2004) % - The theory has been completely revisited by David Lester (4/4/05) % %----------------------------------------------------------------------------- BEGIN IMPORTING exp_term, sincos, trig_ineq, reals@sigma_nat, analysis@derivatives,trig_extra,analysis@derivative_props m,n: VAR nat pm: VAR posnat a: VAR real px: VAR posreal n0x: VAR nzreal nnx: VAR nnreal IMPORTING analysis@deriv_domains 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: LEMMA 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)) sin_px: LEMMA 1/500 > px => sin(px) > px*(1-1/1500000) % Approximation to guarantee cos_lb > 0 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 % Approximation to guarantee sin_lb > 0 Sin_pos_n : MACRO posnat = 11 sin_term_pi_lb: LEMMA n >= Sin_pos_n IMPLIES sin_term(pi_lbn(n+1))(2*n+2) < sin(pi_lbn(n+1)) sin_lb_pi_not_pos: LEMMA FORALL (b9:below(11)): NOT sin_lb(pi_lbn(b9+1),b9) > 0 sin_lb_pi_pos: LEMMA n >= Sin_pos_n IMPLIES sin_lb(pi_lbn(n+1),n) > 0 pi_lb_est(n:nat): {rr:nnreal | rr < pi} = IF n < 12 THEN pi_lbn(n)-2/(n^3+1) ELSE pi_lbn(n) ENDIF pi_lb_est_le: LEMMA pi_lb_est(n) <= pi_lbn(n) AND pi_lb_est(n) <= pi sin_lb_pi_est_pos: LEMMA sin_lb(pi_lb_est(n+1),n) > 0 sin_lb_pi_range_pos: LEMMA px <= pi_lb_est(n+1) IMPLIES sin_lb(px,n) > 0 % Monotonicity of cos_ub cos_ub_nn_strict_decreasing: LEMMA n>=1 IMPLIES strict_decreasing?(LAMBDA (x:{x:nnreal| x <= pi_lb_est(n)}): cos_ub(x,n)) cos_ub_np_strict_increasing: LEMMA n>=1 IMPLIES strict_increasing?(LAMBDA (x:{x:npreal| x >= -pi_lb_est(n)}): cos_ub(x,n)) % Monotonicity of sin_lb and sin_ub sin_lb_increasing: LEMMA strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_l sin_ub_increasing: LEMMA strict_increasing?(LAMBDA (x:{x:real| -pi_lb_est(n)/2 <= x AND x <= pi_lb_est(n)/2}): sin_u sin_lb_nn_decreasing: LEMMA strict_decreasing?(LAMBDA (x:{x:real | pi/2 <= x AND x <= pi}): sin_lb(x,n)) cos_term_pi_ub: LEMMA n >= Cos_pos_n IMPLIES -cos_term(pi_ubn(n)/2)(2*n+1) < -cos(pi_ubn(n)/2) cos_ub_pi2_neg : LEMMA n >= Cos_pos_n IMPLIES cos_ub(pi_ubn(n)/2,n) < 0 pi_ub_est(n:nat): {rr:nnreal | pi < rr AND rr < 3*pi/2} = IF n < 5 THEN pi_ubn(n)+1/(n+1)^4 ELSE pi_ubn(n) ENDIF sin_ub_nn_decreasing: LEMMA n>=1 IMPLIES strict_decreasing?(LAMBDA (x:{x:real | pi_ub_est(n)/2 <= x AND x <= pi_lb_est(n)}): sin_ub(x END trig_approx ¤ Dauer der Verarbeitung: 0.13 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.Bot Zugriff |
