Quelle  ln_exp.pvs   Sprache: 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@fundamental_theorem, 
%             analysis@chain_rule, 
%             analysis@derivatives_more

    IMPORTING reals@real_fun_ops, reals@real_fun_preds

%   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           : AXIOM ln(1) = 0

   ln_mult        : AXIOM 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: AXIOM strict_increasing?(ln)
  
   ln_increasing  : LEMMA increasing?(ln)

   ln_image_all   : AXIOM 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      : AXIOM 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