|
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.18 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
