% 
% 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