|
tan_approx : THEORY
%-----------------------------------------------------------------------------
% tan_approx
% -----------
% tangent approximations
% Cesar Munoz (Feb 6 2004)
%
%-----------------------------------------------------------------------------
BEGIN
IMPORTING trig_approx
n : VAR nat
a,b : VAR real
% Approximations tan
tan_lb_ub(a:real,(n|cos_ub(a,n) /= 0)): real = sin_lb(a,n)/cos_ub(a,n)
tan_ub_lb(a:real,(n|cos_lb(a,n) /= 0)): real = sin_ub(a,n)/cos_lb(a,n)
tan_lb_lb(a:real,(n|cos_lb(a,n) /= 0)): real = sin_lb(a,n)/cos_lb(a,n)
tan_ub_ub(a:real,(n|cos_ub(a,n) /= 0)): real = sin_ub(a,n)/cos_ub(a,n)
tan_lb_ub_neg : LEMMA
cos_ub(a,n) /= 0 IMPLIES
tan_lb_ub(-a,n) = -tan_ub_ub(a,n)
tan_ub_lb_neg : LEMMA
cos_lb(a,n) /= 0 IMPLIES
tan_ub_lb(-a,n) = -tan_lb_lb(a,n)
tan_lb_lb_neg : LEMMA
cos_lb(a,n) /= 0 IMPLIES
tan_lb_lb(-a,n) = -tan_ub_lb(a,n)
tan_ub_ub_neg : LEMMA
cos_ub(a,n) /= 0 IMPLIES
tan_ub_ub(-a,n) = -tan_lb_ub(a,n)
tan_bounds_0_pi2 : LEMMA
0 <= a AND a < pi/2 AND cos_lb(a,n) > 0 IMPLIES
tan_lb_ub(a,n) <= tan(a) AND
tan(a) <= tan_ub_lb(a,n)
tan_bounds_npi2_0 : LEMMA
-pi/2 < a AND a <= 0 AND cos_lb(a,n) > 0 IMPLIES
tan_lb_lb(a,n) <= tan(a) AND
tan(a) <= tan_ub_ub(a,n)
tan_bounds_pi2_pi : LEMMA
pi/2 < a AND a <= pi AND cos_ub(a,n) < 0 IMPLIES
tan_ub_ub(a,n) <= tan(a) AND
tan(a) <= tan_lb_lb(a,n)
tan_bounds_npi_npi2 : LEMMA
-pi <= a AND a < -pi/2 AND cos_ub(a,n) < 0 IMPLIES
tan_ub_lb(a,n) <= tan(a) AND
tan(a) <= tan_lb_ub(a,n)
END tan_approx
¤ Dauer der Verarbeitung: 0.3 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.
|
