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 CONTAINING 1CONTAINING -1CONTAINING 0LEMMA not_one_element?[posreal]LEMMA connected?[posreal]VAR nzreal_gt_m1VAR nzreal_lt1VAR posrealVAR nzrealVAR posnatVAR real_abs_lt1LEMMA xgtm1/(1+xgtm1) < ln(1+xgtm1) AND % 4.1.33 LEMMA xlt1 < -ln(1-xlt1) AND -ln(1-xlt1) < xlt1/(1-xlt1) % 4.1.34 LEMMA px <= 5828/10000 IMPLIES abs(ln(1-px)) < 3*px/2 % 4.1.35 LEMMA ln(px) <= px-1 % 4.1.36 LEMMA ln(px) <= pn*(exp(ln(px)/pn)-1) % 4.1.37 LEMMA abs(ln(1+xalt1)) <= -ln(1-abs(xalt1)) % 4.1.38 LEMMA exp(-xlt1/(1-xlt1)) < 1-xlt1 AND % 4.2.29 LEMMA nzx+1 < exp(nzx) % 4.2.30 LEMMA exp(xlt1) < 1/(1-xlt1) % 4.2.31 END ln_exp_ineqquality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
