atan2 : THEORY %----------------------------------------------------------------------------- % atan2 % ---- % - defines two-argument inverse tangent (arctangent): atan2 %----------------------------------------------------------------------------- BEGIN
IMPORTING trig_basic, atan, asin, acos
x,y : VAR real
a : VAR {z:nnreal| z < 2*pi}
nz : VAR negreal
pz : VAR posreal
%% Arc tangent of y/x taking into in account quadrants and indefinitions %% Polar angle of x + yI.
atan2(x:real,y:{z:real|x=0 => z/=0}): real
= IF x > 0 THENIF y >= 0 THEN atan(y/x) ELSE 2*pi+atan(y/x) ENDIF ELSIF x = 0 THENIF y > 0 THEN pi/2 ELSE 3*pi/2 ENDIF ELSE pi + atan(y/x) ENDIF
atan2_0_2pi : LEMMA
(x /= 0 OR y /= 0) IMPLIES
(((x>=0 AND y>=0) => (0 <= atan2(x,y) AND atan2(x,y) <= pi/2)) AND
((x< 0 AND y>=0) => (pi/2 < atan2(x,y) AND atan2(x,y) <= pi)) AND
((x< 0 AND y< 0) => (pi < atan2(x,y) AND atan2(x,y) < 3*pi/2)) AND
((x>=0 AND y< 0) => (3*pi/2 <= atan2(x,y) AND atan2(x,y) < 2*pi)))
atan2_ge_0_lt_2pi : LEMMA
(x /= 0 OR y /= 0) IMPLIES
atan2(x,y) >= 0 and
atan2(x,y) < 2*pi
nnreal_lt_2pi: NONEMPTY_TYPE = {x:nnreal | x < 2*pi}
atan2_swap_zero : LEMMA
(x = 0 AND y /= 0 IMPLIES
atan2(x,y) = atan2(y,x) + pi/2) AND
(y = 0 AND x /= 0 IMPLIES
atan2(x,y) = atan2(y,x) - pi/2)
atan2_cos_sin : LEMMA
atan2(cos(a),sin(a)) = a
sin_atan2 : LEMMA
(x /= 0 OR y /= 0) IMPLIES
sin(atan2(x,y)) = IF x=0 THEN IF y > 0 THEN 1 ELSE -1 ENDIF ELSE LET yx = y/x IN LET r = yx/sqrt((sq(yx)+1)) IN IF x > 0 THEN r ELSE -r ENDIF ENDIF
cos_atan2 : LEMMA
(x /= 0 OR y /= 0) IMPLIES
cos(atan2(x,y)) = IF x = 0 THEN 0 ELSE LET yx = y/x IN IF x > 0 THEN 1/sqrt((sq(yx)+1)) ELSE -1/sqrt((sq(yx)+1)) ENDIF ENDIF
END atan2
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
