|
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.23 Sekunden
(vorverarbeitet)
¤
|
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.
|
