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@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

¤ 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.