|
%------------------------------------------------------------------------------
% Generalized log function (without ln/exp)
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%
%------------------------------------------------------------------------------
nn_log: THEORY
BEGIN
IMPORTING rational_props_aux,
nn_root,
nn_rational_expt,
nnreal_expt
a,b,x,y,z: VAR nnreal
q: VAR nnrat
px,py,pa,pb,
delta,r,
epsilon: VAR posreal
ne1x: VAR {r | r /= 1}
gt1x,gt1y: VAR {r | r > 1}
lt1x,lt1y: VAR {r | r < 1}
log_gt1(gt1x):[{r | r>=1}->nnreal]
= inverse[nnreal,{r | r>=1}](lambda x: nnreal_expt(gt1x,x))
log_lt1(lt1x):[{r | r<=1}->nnreal]
= inverse[nnreal,{r | r<=1}](lambda x: nnreal_expt(lt1x,x))
nn_log(ne1x)(y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):nnreal
= IF ne1x>1 THEN log_gt1(ne1x)(y) ELSE log_lt1(ne1x)(y) ENDIF
nn_log_expt: LEMMA nn_log(ne1x)(nnreal_expt(ne1x,y)) = y
nn_expt_log: LEMMA FORALL (y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):
nnreal_expt(ne1x,nn_log(ne1x)(y)) = y
nn_log_plus: LEMMA FORALL (x,y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):
nn_log(ne1x)(x*y) = nn_log(ne1x)(x) + nn_log(ne1x)(y)
nn_log_1: LEMMA nn_log(ne1x)(1) = 0
nn_log_ne1x: LEMMA nn_log(ne1x)(ne1x) = 1
nn_log_gt1: LEMMA nn_log(gt1x)(gt1y) > 1 IFF gt1y > gt1x
nn_inv_base_log: LEMMA
FORALL (y:{r | ne1x>1 AND r<=1 OR ne1x<1 AND r>=1}):
nn_log(1/ne1x)(y) = nn_log(ne1x)(1/y)
nn_log_increasing: LEMMA 1 < x AND x < y =>
nn_log(gt1x)(x) < nn_log(gt1x)(y)
END nn_log
¤ Dauer der Verarbeitung: 0.0 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.
|
