|
%------------------------------------------------------------------------------
% Complex logarithm and exponential functions
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 5/29/04 Initial version (DRL)
%------------------------------------------------------------------------------
exp: THEORY
BEGIN
IMPORTING polar,
trig@trig_ineq,
trig_aux,
lnexp@ln_exp
r: VAR real
x,y,z: VAR complex
n0x,n0y,n0z: VAR nzcomplex
theta: VAR argrng
j: VAR int
exp(z): nzcomplex = exp(Re(z))*(cos(Im(z))+i*sin(Im(z)))
exp_real : LEMMA exp(r) = ln_exp.exp(r)
exp_imag : LEMMA exp(r*i) = cos(r) + i*sin(r)
abs_exp_imag : LEMMA abs(exp(r*i)) = 1
arg_exp_real : LEMMA arg(exp(r)) = 0
arg_exp_imag : LEMMA arg(exp(theta*i)) = theta
exp_0 : LEMMA exp(0) = 1
exp_1 : LEMMA exp(1) = e
exp_i_pi : LEMMA exp(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*i) = exp(x)
abs_exp : LEMMA abs(exp(z)) = ln_exp.exp(Re(z))
ln(n0z): complex = ln(abs(n0z)) + arg(n0z)*i
ln_1 : LEMMA ln(1) = 0
ln_e : LEMMA ln(e) = 1
ln_exp : LEMMA (2*j-1)*pi < Im(z) AND Im(z) <= (2*j+1)*pi IMPLIES
ln(exp(z)) = z - 2*j*pi*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*i
ELSIF r <= -pi THEN -2*pi*i
ELSE 0 ENDIF
ln_inv : LEMMA ln(1/n0x) = IF arg(n0x) = pi THEN 2*pi
ELSE 0 ENDIF*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*i
ELSIF r <= -pi THEN -2*pi*i
ELSE 0 ENDIF
END exp
¤ Dauer der Verarbeitung: 0.1 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.
|
