|
%
% David Lester, Manchester University
% 10/10/08
%
% Linking log and ^ to exp and ln.
ln_exp_def: THEORY
BEGIN
IMPORTING log,
real_expt,
lnexp_fnd@ln_exp
i: VAR int
n: VAR nat
q: VAR nnrat
pn: VAR posnat
x: VAR real
z: VAR nnreal
a,r,y: VAR posreal
ne1x: VAR {r | r /= 1}
expt_exp: LEMMA expt(y,n) = exp(n*ln(y))
nn_root_def: LEMMA nn_root(z,pn) = IF z = 0 THEN 0 ELSE exp(ln(z)/pn) ENDIF
nn_rational_expt_def: LEMMA nn_rational_expt(y,q) = exp(q*ln(y))
nnreal_expt_def: LEMMA nnreal_expt(y,z) = exp(z*ln(y))
real_expt_def: LEMMA y^x = exp(x*ln(y))
nn_log_def: LEMMA r > 1 AND y >= 1 OR r < 1 AND y <= 1 =>
nn_log(r)(y) = ln(y)/ln(r)
log_def: LEMMA log(ne1x,y) = ln(y)/ln(ne1x)
IMPORTING analysis@continuous_functions,
analysis@derivatives
log_continuous: LEMMA continuous?[posreal](log(ne1x))
log_derivable: LEMMA derivable?[posreal](log(ne1x)) AND
deriv[posreal](log(ne1x)) = (LAMBDA y: 1/(ln(ne1x)*y))
real_expt_continuous: LEMMA continuous?[posreal](lambda y: y^x)
real_expt_derivable: LEMMA derivable?[posreal](lambda y: y^x) AND
deriv[posreal](lambda y: y^x)
= (lambda y: x*y^(x-1))
END ln_exp_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
