Impressum ln_exp.pvs

ln_exp: THEORY
%------------------------------------------------------------------------
%   Definition of Logarithm and Exponential functions
%
%   Author:  Ricky W. Butler              NASA Langley Research Center
%------------------------------------------------------------------------
BEGIN

   x,y,a: VAR real
   i: VAR integer
   px,py,p1,p2: VAR posreal


   IMPORTING analysis@integral, 
             analysis@indefinite_integral, 
             analysis@chain_rule, 
             analysis@derivative_props, analysis@deriv_domains

   conn_posreal: LEMMA connected?[posreal]

   AUTO_REWRITE+ conn_posreal

   one_over_t_cont: LEMMA continuous?((LAMBDA (t: posreal): 1 / t))

   ln_prep: LEMMA FORALL (x: posreal):
         Integrable?[posreal](1, x, (LAMBDA (t: posreal): 1 / t));


   ln(x: posreal): real = Integral(1,x, (LAMBDA (t: posreal): 1/t))

   ln_derivable   : LEMMA derivable?(ln) AND
                       deriv(ln) = (LAMBDA (t: posreal): 1/t)

   ln_continuous  : LEMMA continuous?(ln)
 
   ln_1           : LEMMA ln(1) = 0

   ln_mult        : LEMMA ln(px*py) = ln(px) + ln(py)
   ln_div         : LEMMA ln(px/py) = ln(px) - ln(py)
   ln_expt        : LEMMA ln(px^i)  = i*ln(px) 

   ln_strict_increasing: LEMMA strict_increasing?(ln)
  
   ln_increasing  : LEMMA increasing?(ln)

   ln_image_all   : LEMMA EXISTS (px: posreal): ln(px) = y

   ln_bij         : LEMMA bijective?[posreal, real](ln)

   large_ln       : LEMMA (FORALL a: EXISTS px: a < ln(px))

   ln_eq_0        : LEMMA ln(px) = 0 IMPLIES px = 1

   ln_ge_0        : LEMMA px >= 1 IMPLIES ln(px) >= 0

   ln_gt_0        : LEMMA px > 1 IMPLIES ln(px) > 0

   exp(x): { py | x = ln(py)}

   e: posreal = exp(1)

   exp_def        : LEMMA exp = inverse(ln)

   exp_bij        : LEMMA bijective?[real,posreal](exp)

   ln_exp         : LEMMA ln(exp(x)) = x

   exp_ln         : LEMMA exp(ln(py)) = py

   ln_e           : LEMMA ln(e) = 1

   ln_2_bnds      : LEMMA 1/2 <= ln(2) AND ln(2) <= 1

   exp_int        : LEMMA exp(i) = e^i

   exp_sum        : LEMMA exp(x+y) = exp(x)*exp(y) 

   exp_diff       : LEMMA exp(x-y) = exp(x)/exp(y) 

   exp_scal       : LEMMA exp(i*x) = exp(x)^i

   exp_0          : LEMMA exp(0) = 1

   exp_1          : LEMMA exp(1) = e

   exp_neg        : LEMMA exp(-x) = 1/exp(x)

   expt_alt_def   : LEMMA x > 0 IMPLIES x^i = exp(i*ln(x))

   exp_strict_increasing : LEMMA strict_increasing?(exp)

   exp_increasing : LEMMA increasing?(exp)

   exp_continuous : LEMMA continuous?(exp)

   IMPORTING analysis@derivative_inverse

   exp_deriv      : LEMMA derivable?(exp) AND deriv(exp) = exp

   e_bnds         : LEMMA 2 <= e AND e <= 4

   large_exp      : LEMMA (FORALL a: EXISTS x: a < exp(x))

   small_exp      : LEMMA (FORALL px: EXISTS x: exp(x) < px)

   AUTO_REWRITE+ exp_0
   AUTO_REWRITE+ exp_1
   AUTO_REWRITE+ ln_1
   AUTO_REWRITE+ ln_e

END ln_exp