|
%
% 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
¤ Dauer der Verarbeitung: 0.13 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.
|
