Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.