Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ln_exp.pvs Sprache: PVS

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

¤ Dauer der Verarbeitung: 0.0 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.