|
ln_exp_ineq: THEORY
%------------------------------------------------------------------------------
% Inequalities involving ln and exp
%
% Author: David Lester
%
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING ln_exp, analysis@derivative_props, analysis@chain_rule,
% ln_series, exp_series
ln_exp_series_alt
nzreal_gt_m1: NONEMPTY_TYPE = {x:nzreal | x > -1} CONTAINING 1
nzreal_lt1: NONEMPTY_TYPE = {x:nzreal | x < 1 } CONTAINING -1
real_abs_lt1: NONEMPTY_TYPE = {x:real | -1 < x & x < 1 } CONTAINING 0
noa_posreal : LEMMA not_one_element?[posreal]
conn_posreal: LEMMA connected?[posreal]
AUTO_REWRITE+ noa_posreal
AUTO_REWRITE+ conn_posreal
AUTO_REWRITE+ deriv_domain_posreal
xgtm1: VAR nzreal_gt_m1
xlt1: VAR nzreal_lt1
px: VAR posreal
nzx: VAR nzreal
pn: VAR posnat
xalt1: VAR real_abs_lt1
ln_ineq1: LEMMA xgtm1/(1+xgtm1) < ln(1+xgtm1) AND
ln(1+xgtm1) < xgtm1 % 4.1.33
ln_ineq2: LEMMA xlt1 < -ln(1-xlt1) AND -ln(1-xlt1) < xlt1/(1-xlt1) % 4.1.34
ln_ineq3: LEMMA px <= 5828/10000 IMPLIES abs(ln(1-px)) < 3*px/2 % 4.1.35
ln_ineq4: LEMMA ln(px) <= px-1 % 4.1.36
ln_ineq5: LEMMA ln(px) <= pn*(exp(ln(px)/pn)-1) % 4.1.37
ln_ineq6: LEMMA abs(ln(1+xalt1)) <= -ln(1-abs(xalt1)) % 4.1.38
exp_ineq1: LEMMA exp(-xlt1/(1-xlt1)) < 1-xlt1 AND
1-xlt1 < exp(-xlt1) % 4.2.29
exp_ineq2: LEMMA nzx+1 < exp(nzx) % 4.2.30
exp_ineq3: LEMMA exp(xlt1) < 1/(1-xlt1) % 4.2.31
END ln_exp_ineq
¤ Dauer der Verarbeitung: 0.0 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.
|
