| products/sources/formale Sprachen/Isabelle/Pure/PIDE/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 13 kB |
|
Impressum complex_lnexp.pvs
Interaktion und |
|||||||||
|
%------------------------------------------------------------------------------
% 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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.14Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28