|
%------------------------------------------------------------------------------
% Complex logarithm and exponential functions
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 5/29/04 Initial version (DRL)
%------------------------------------------------------------------------------
complex_lnexp: THEORY
BEGIN
IMPORTING polar, trig@trig_ineq, trig_aux, lnexp@hyperbolic
r: VAR real
x,y,z: VAR complex
n0x,n0y,n0z: VAR nzcomplex
theta: VAR argrng
j: VAR int
exp(z): nzcomplex = complex_(exp(Re(z))*cos(Im(z)),
exp(Re(z))*sin(Im(z)))
Re_exp: LEMMA Re(exp(z)) = exp(Re(z))*cos(Im(z))
Im_exp: LEMMA Im(exp(z)) = exp(Re(z))*sin(Im(z))
AUTO_REWRITE+ Re_exp
AUTO_REWRITE+ Im_exp
exp_i_pi : LEMMA exp(complex_i*pi) = -1
exp_plus : LEMMA exp(x+y) = exp(x)*exp(y)
exp_negate : LEMMA exp(-x) = 1/exp(x)
exp_minus : LEMMA exp(x-y) = exp(x)/exp(y)
exp_periodicity : LEMMA exp(x+(2*j*pi)*complex_i) = exp(x)
abs_exp : LEMMA abs(exp(z)) = exp(Re(z))
arg_exp : LEMMA -pi < Im(z) AND Im(z) <= pi =>
arg(exp(z)) = Im(z)
ln(n0z): complex = complex_(ln(abs(n0z)),arg(n0z))
Re_ln: LEMMA Re(ln(n0z)) = ln(abs(n0z))
Im_ln: LEMMA Im(ln(n0z)) = arg(n0z)
AUTO_REWRITE+ Re_ln
AUTO_REWRITE+ Im_ln
AUTO_REWRITE+ abs_exp
AUTO_REWRITE+ arg_exp
ln_exp : LEMMA (2*j-1)*pi < Im(z) AND Im(z) <= (2*j+1)*pi =>
ln(exp(z)) = z - (2*j*pi)*complex_i
exp_ln : LEMMA exp(ln(n0z)) = n0z
ln_mult : LEMMA ln(n0x*n0y) = ln(n0x) + ln(n0y) -
LET r = arg(n0x)+arg(n0y) IN
IF r > pi THEN 2*pi
ELSIF r <= -pi THEN -2*pi
ELSE 0 ENDIF*complex_i
ln_inv : LEMMA ln(1/n0x) = IF arg(n0x) = pi THEN 2*pi
ELSE 0 ENDIF*complex_i - ln(n0x)
ln_div : LEMMA ln(n0x/n0y) = ln(n0x) - ln(n0y) -
LET r = arg(n0x)-arg(n0y) IN
IF r > pi THEN 2*pi
ELSIF r <= -pi THEN -2*pi
ELSE 0 ENDIF*complex_i
sin(z): complex = complex_(sin(Re(z))*cosh(Im(z)),-cos(Re(z))*sinh(Im(z)))
cos(z): complex = complex_(cos(Re(z))*cosh(Im(z)),-sin(Re(z))*sinh(Im(z)))
Re_sin: LEMMA Re(sin(z)) = sin(Re(z))*cosh(Im(z))
Im_sin: LEMMA Im(sin(z)) = -cos(Re(z))*sinh(Im(z))
Re_cos: LEMMA Re(cos(z)) = cos(Re(z))*cosh(Im(z))
Im_cos: LEMMA Im(cos(z)) = -sin(Re(z))*sinh(Im(z))
AUTO_REWRITE+ Re_sin
AUTO_REWRITE+ Im_sin
AUTO_REWRITE+ Re_cos
AUTO_REWRITE+ Re_sin
sinh(z):complex = (exp(z) - exp(-z))/2 % 4.5.1
cosh(z):complex = (exp(z) + exp(-z))/2 % 4.5.2
Re_sinh: LEMMA Re(sinh(z)) = sinh(Re(z))*cos(Im(z))
Im_sinh: LEMMA Im(sinh(z)) = cosh(Re(z))*sin(Im(z))
Re_cosh: LEMMA Re(cosh(z)) = cosh(Re(z))*cos(Im(z))
Im_cosh: LEMMA Im(cosh(z)) = sinh(Re(z))*sin(Im(z))
AUTO_REWRITE+ Re_sinh
AUTO_REWRITE+ Im_sinh
AUTO_REWRITE+ Re_cosh
AUTO_REWRITE+ Im_cosh
sinh_eq_0: LEMMA sinh(z) = 0 <=> EXISTS j: z = complex_i*(j*pi)
cosh_eq_0: LEMMA cosh(z) = 0 <=> EXISTS j: z = complex_i*((j+1/2)*pi)
Sinh?(z):bool = sinh(z) /= 0
Cosh?(z):bool = cosh(z) /= 0
sx,sy,sz: VAR (Sinh?)
cx,cy,cz: VAR (Cosh?)
tanh(cz):complex = sinh(cz)/cosh(cz) % 4.5.3
csch(sz):complex = 1/sinh(sz) % 4.5.4
sech(cz):complex = 1/cosh(cz) % 4.5.5
coth(sz):complex = cosh(sz)/sinh(sz) % 4.5.6
% Special Values of the Hyperbolic Functions
c_sinh_0: LEMMA sinh(complex_(0,0)) = 0 % 4.5.61
c_cosh_0: LEMMA cosh(complex_(0,0)) = 1 % 4.5.61
c_tanh_0: LEMMA tanh(complex_(0,0)) = 0 % 4.5.61
c_sech_0: LEMMA sech(complex_(0,0)) = 1 % 4.5.61
% Relations between Hyperbolic Functions
c_cosh_sinh_one: LEMMA sq(cosh(z)) - sq(sinh(z)) = 1 % 4.5.16
c_tanh_sech_one: LEMMA sq(tanh(cz)) + sq(sech(cz)) = 1 % 4.5.17
c_coth_csch_one: LEMMA sq(coth(sz)) - sq(csch(sz)) = 1 % 4.5.18
c_cosh_plus_sinh: LEMMA cosh(z) + sinh(z) = exp(z) % 4.5.19
c_cosh_minus_sinh: LEMMA cosh(z) - sinh(z) = exp(-z) % 4.5.20
% Negative Angle Formulas
c_sinh_neg: LEMMA sinh(-z) = -sinh(z) % 4.5.21
c_cosh_neg: LEMMA cosh(-z) = cosh(z) % 4.5.22
c_tanh_neg: LEMMA tanh(-cz) = -tanh(cz) % 4.5.23
c_csch_neg: LEMMA csch(-sz) = -csch(sz)
c_sech_neg: LEMMA sech(-cz) = sech(cz)
c_coth_neg: LEMMA coth(-sz) = -coth(sz)
AUTO_REWRITE+ c_sinh_neg
AUTO_REWRITE+ c_cosh_neg
AUTO_REWRITE+ c_tanh_neg
AUTO_REWRITE+ c_csch_neg
AUTO_REWRITE+ c_sech_neg
AUTO_REWRITE+ c_coth_neg
% Addition Formulas
c_sinh_sum: LEMMA sinh(x+y) = sinh(x)*cosh(y) + cosh(x)*sinh(y) % 4.5.24
c_sinh_diff: LEMMA sinh(x-y) = sinh(x)*cosh(y) - cosh(x)*sinh(y)
c_cosh_sum: LEMMA cosh(x+y) = cosh(x)*cosh(y) + sinh(x)*sinh(y) % 4.5.25
c_cosh_diff: LEMMA cosh(x-y) = cosh(x)*cosh(y) - sinh(x)*sinh(y)
% c_tanh_sum: LEMMA tanh(cx)*tanh(cy) /= -1 => % 4.5.26
% tanh(cx+cy) = (tanh(cx)+tanh(cy))/(1+tanh(cx)*tanh(cy))
% c_coth_sum: LEMMA n0x+n0y /= 0 IMPLIES % 4.5.27
% coth(n0x+n0y)
% = (1+coth(n0x)*coth(n0y))/(coth(n0x)+coth(n0y))
% Half-angle Formulas
% sinh_half: LEMMA sinh(x/2) = LET y = sqrt((cosh(x)-1)/2) IN % 4.5.28
% IF x >= 0 THEN y ELSE -y ENDIF
% cosh_half: LEMMA cosh(x/2) = sqrt((cosh(x)+1)/2) % 4.5.29
% tanh_half1: LEMMA tanh(x/2) = LET y = sqrt((cosh(x)-1)/(cosh(x)+1)) % 4.5.30
% IN IF x >= 0 THEN y ELSE -y ENDIF
% tanh_half2: LEMMA tanh(n0x/2) = (cosh(n0x)-1)/sinh(n0x) % 4.5.30
% tanh_half3: LEMMA tanh(x/2) = sinh(x)/(cosh(x)+1) % 4.5.30
% Multiple-angle Formulas
c_sinh2x: LEMMA sinh(2*x) = 2*sinh(x)*cosh(x) % 4.5.31
% sinh2x_B: LEMMA sinh(2*x) = 2*tanh(x)/(1-sq(tanh(x))) % 4.5.31
c_cosh2x: LEMMA cosh(2*x) = 2*sq(cosh(x))-1 % 4.5.32
c_cosh2x_B: LEMMA cosh(2*x) = 2*sq(sinh(x))+1 % 4.5.32
c_cosh2x_C: LEMMA cosh(2*x) = sq(cosh(x)) + sq(sinh(x)) % 4.5.32
% tanh2x: LEMMA tanh(2*x) = 2*tanh(x)/(1+sq(tanh(x))) % 4.5.33
% sinh3x: LEMMA sinh(3*x) = 3*sinh(x) + 4*sinh(x)^3 % 4.5.34
% cosh3x: LEMMA cosh(3*x) = 4*cosh(x)^3-3*cosh(x) % 4.5.35
c_sinh4x: LEMMA sinh(4*x) % 4.5.36
= 4*sinh(x)*cosh(x)*(sq(sinh(x)) + sq(cosh(x)))
complex_sin_def: LEMMA sin(z) = -complex_i * sinh(complex_i*conjugate(z))
complex_cos_def: LEMMA cos(z) = cosh(complex_i*z)
END complex_lnexp
¤ 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.
|
