ln_exp: THEORY %------------------------------------------------------------------------ % Definition of Logarithm and Exponential functions % % Author: Ricky W. Butler NASA Langley Research Center %------------------------------------------------------------------------ BEGIN VAR realVAR integerVAR 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)); % = 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) AXIOM ln(1) = 0AXIOM ln(px*py) = ln(px) + ln(py)LEMMA ln(px/py) = ln(px) - ln(py)LEMMA ln(px^i) = i*ln(px) AXIOM strict_increasing?(ln)LEMMA increasing?(ln)AXIOM EXISTS (px: posreal): ln(px) = yLEMMA bijective?[posreal, real](ln)LEMMA (FORALL a: EXISTS px: a < ln(px))LEMMA ln(px) = 0 IMPLIES px = 1LEMMA px >= 1 IMPLIES ln(px) >= 0LEMMA px > 1 IMPLIES ln(px) > 0LEMMA exp = inverse(ln)LEMMA bijective?[real,posreal](exp)LEMMA ln(exp(x)) = xLEMMA exp(ln(py)) = pyLEMMA ln(e) = 1AXIOM 1/2 <= ln(2) AND ln(2) <= 1LEMMA exp(i) = e^iLEMMA exp(x+y) = exp(x)*exp(y) LEMMA exp(x-y) = exp(x)/exp(y) LEMMA exp(i*x) = exp(x)^iLEMMA exp(0) = 1LEMMA exp(1) = eLEMMA exp(-x) = 1/exp(x)LEMMA x > 0 IMPLIES x^i = exp(i*ln(x))LEMMA strict_increasing?(exp)LEMMA increasing?(exp)% exp_continuous : LEMMA continuous(exp) % IMPORTING analysis@derivative_inverse % exp_deriv : LEMMA derivable(exp) AND deriv(exp) = exp LEMMA 2 <= e AND e <= 4LEMMA (FORALL a: EXISTS x: a < exp(x))LEMMA (FORALL px: EXISTS x: exp(x) < px)END ln_expquality 89%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
