Quelle  ln_exp_ineq.pvs

ln_exp_ineq: THEORY
%------------------------------------------------------------------------------

% Inequalities involving ln and exp
%
% Author: David Lester
%
% 
%------------------------------------------------------------------------------

  BEGIN

  IMPORTING ln_exp, analysis@derivative_props, analysis@chain_rule,
%            ln_series, exp_series
            ln_exp_series_alt

  nzreal_gt_m1: NONEMPTY_TYPE = {x:nzreal | x > -1}          CONTAINING  1
  nzreal_lt1:   NONEMPTY_TYPE = {x:nzreal | x < 1 }          CONTAINING -1
  real_abs_lt1: NONEMPTY_TYPE = {x:real   | -1 < x & x < 1 } CONTAINING  0


   noa_posreal : LEMMA not_one_element?[posreal]
   conn_posreal: LEMMA connected?[posreal]

   AUTO_REWRITE+ noa_posreal
   AUTO_REWRITE+ conn_posreal
   AUTO_REWRITE+ deriv_domain_posreal


  xgtm1: VAR nzreal_gt_m1
  xlt1:  VAR nzreal_lt1
  px:    VAR posreal
  nzx:   VAR nzreal
  pn:    VAR posnat
  xalt1: VAR real_abs_lt1

  ln_ineq1:  LEMMA xgtm1/(1+xgtm1) < ln(1+xgtm1) AND
                   ln(1+xgtm1) < xgtm1                                 % 4.1.33

  ln_ineq2:  LEMMA xlt1 < -ln(1-xlt1) AND -ln(1-xlt1) < xlt1/(1-xlt1)  % 4.1.34

  ln_ineq3:  LEMMA px <= 5828/10000 IMPLIES abs(ln(1-px)) < 3*px/2     % 4.1.35

  ln_ineq4:  LEMMA ln(px) <= px-1                                      % 4.1.36

  ln_ineq5:  LEMMA ln(px) <= pn*(exp(ln(px)/pn)-1)                     % 4.1.37

  ln_ineq6:  LEMMA abs(ln(1+xalt1)) <= -ln(1-abs(xalt1))               % 4.1.38

  exp_ineq1: LEMMA exp(-xlt1/(1-xlt1)) < 1-xlt1 AND
                   1-xlt1 < exp(-xlt1)                                 % 4.2.29

  exp_ineq2: LEMMA nzx+1 < exp(nzx)                                    % 4.2.30

  exp_ineq3: LEMMA exp(xlt1) < 1/(1-xlt1)                              % 4.2.31

  END ln_exp_ineq