|
%------------------------------------------------------------------------------
% Polar coordinate complex numbers
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 5/29/04 Initial version (DRL)
% Version 1.1 4/10/07 abs_i, arg_i added (DRL)
%
% Narkawicz 12/2013 +
%------------------------------------------------------------------------------
polar: THEORY
BEGIN
IMPORTING arithmetic, reals@sqrt, trig@atan2,
trig@atan2_props,
number_fields_sq
argrng: TYPE+ = {x:real | -pi < x & x <= pi} CONTAINING 0
z,z1,z2: VAR complex
n0x,n0y,n0z: VAR nzcomplex
nnx: VAR nnreal
nx: VAR negreal
r,x,y: VAR real
j: VAR int
theta: VAR argrng
nzreal_is_nzcomplex: JUDGEMENT nzreal SUBTYPE_OF nzcomplex
abs(z):nnreal = sqrt(z*conjugate(z))
abs_def: LEMMA abs(z) = sqrt(sq.sq(Re(z))+sq.sq(Im(z)))
abs_real_rew: LEMMA abs(r) = real_defs.abs(r)
abs_imag_rew: LEMMA abs(r*i) = real_defs.abs(r)
abs_nzcomplex: LEMMA abs(n0z) > 0
abs_nz_iff_nz: LEMMA abs(z) > 0 IFF z /= 0
abs_is_0: LEMMA abs(z) = 0 IFF z = 0
abs_neg: LEMMA abs(-z) = abs(z)
abs_mult: LEMMA abs(z1*z2) = abs(z1)*abs(z2)
abs_inv: LEMMA abs(1/n0z) = 1/abs(n0z)
abs_div: LEMMA abs(z/n0z) = abs(z)/abs(n0z)
abs_triangle: LEMMA abs(z1+z2) <= abs(z1) + abs(z2)
abs_triangle_minus: LEMMA abs(z1-z2)>=abs(z1)-abs(z2)
abs_abs: LEMMA abs(abs(z)) = abs(z)
abs_i: LEMMA abs(i) = 1
% Lemmata "abs_is_0", "abs_neg" and "abs_triangle" suffice to demonstrate
% that the complex numbers form a (normed) metric space, with metric
% "d(x,y) = abs(x-y)".
% We define a complex number's principal argument value as "arg", note:
% lower case "a" for a real number.
%
% Observe unpleasant formulation of properties to cope with multiples of 2*pi.
arg(z):argrng = IF z = 0 THEN 0
ELSIF Im(z) < 0 THEN atan2(Re(z),Im(z)) - 2*pi
ELSE atan2(Re(z),Im(z)) ENDIF
arg_is_0_nz: LEMMA arg(n0z) = 0 IFF (Re(n0z) > 0 AND Im(n0z) = 0)
arg_is_0: LEMMA arg(z) = 0 IFF (Re(z) >= 0 AND Im(z) = 0)
arg_is_pi2: LEMMA arg(z) = pi/2 IFF (Re(z) = 0 AND Im(z) > 0)
arg_is_pi: LEMMA arg(z) = pi IFF (Re(z) < 0 AND Im(z) = 0)
arg_is_mpi2: LEMMA arg(z) = -pi/2 IFF (Re(z) = 0 AND Im(z) < 0)
arg_lt_0: LEMMA arg(z) < 0 IFF Im(z) < 0
arg_p_lt_pi: LEMMA (0 < arg(z) AND arg(z) < pi) IFF Im(z) > 0
arg_gt_0: LEMMA arg(z) > 0 IFF (Im(z) > 0 OR (Im(z) = 0 AND Re(z) < 0))
arg_div_abs: LEMMA arg(n0x) = arg(n0x/abs(n0x))
Re_cos_abs1: LEMMA abs(n0x) = 1 IMPLIES Re(n0x) = cos(arg(n0x))
Im_sin_abs1: LEMMA abs(n0x) = 1 IMPLIES Im(n0x) = sin(arg(n0x))
arg_nnreal: LEMMA arg(nnx) = 0
arg_nreal: LEMMA arg(nx) = pi
arg_i: LEMMA arg(i) = pi/2
arg_neg: LEMMA arg(-n0x) = IF 0 < arg(n0x) THEN arg(n0x) - pi
ELSE arg(n0x) + pi ENDIF
arg_mult: LEMMA arg(n0x*n0y) = LET r = arg(n0x)+arg(n0y) IN
IF r > pi THEN r-2*pi
ELSIF r <= -pi THEN r+2*pi
ELSE r ENDIF
arg_inv: LEMMA arg(1/n0z) = IF arg(n0z) = 0 THEN 0
ELSIF arg(n0z) = pi THEN pi
ELSE -arg(n0z) ENDIF
arg_div: LEMMA arg(n0x/n0y) = LET r = arg(n0x)-arg(n0y) IN
IF r > pi THEN r-2*pi
ELSIF r <= -pi THEN r+2*pi
ELSE r ENDIF
polar(z):[nnreal,argrng] = (abs(z),arg(z))
rectangular(z):[real,real] = (Re(z),Im(z))
from_polar(r,theta):complex = r*cos(theta) + r*sin(theta)*i
from_rectangular(x,y):complex = x + y*i
arg_from_polar: LEMMA r>0 AND -pi < theta AND theta<=pi IMPLIES
arg(from_polar(r,theta))=theta
idempotent_rectangular: LEMMA z = from_rectangular(rectangular(z))
idempotent_polar : LEMMA n0z = from_polar(polar(n0z))
END polar
¤ 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.
|
