%------------------------------------------------------------------------------ % Generalized Power function (without ln/exp) % % Author: David Lester, Manchester University & NIA % % Version 1.0 19/08/08 Initial version (DRL) % % This library provides Roots, Powers and Generalized Logs % % The (achieved) aim is to avoid using all libraries except those in % the standard prelude. Hooks are provided so that the power function % along with root and log can be shown to be continuous (over % suitable domains), but no continuity libraries have been used to % construct this library, meaning that it is built directly onto the % standard SRI prelude. % % Features include: % % By INCLUDING root, you can have statements like: % % root(8,3) = 2 % % By INCLUDING real_expt, you can have statements like: % % 8^(1/3) = 2 % % BY INCLUDING log, you can have statements like: % % log(2)(8) = 3 /* = ln(8)/ln(2) */ % %------------------------------------------------------------------------------
top: THEORY
BEGIN
IMPORTING rational_props_aux, % Extra properties for prelude
exponentiation_aux, % Extra properties for prelude
nn_root, % nth-roots of nnreals
root, % nth-roots of reals % (includes negative reals, for odd n)
nn_rational_expt, % x^y (x:nnreal, y: nnrat) Note 0^0 = 1
nnreal_expt, % x^y (x,y: nnreal)
real_expt, % x^y (x:nnreal, y:real) provided y>=0 when 0^y
nn_log, % inverse of nnreal_expt
log, % inverse of real_expt
real_fun_power, % exponentiation of functions
ln_exp_def % linking log to ln and ^ to exp END top
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
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.
