proposition: Lemma Exp_Log_lemma : forall x y Hx Hy, [0] [=] Log y Hy[-]Log x Hx -> y [<=] x.
proof: Proof. intros x y Hx Hy H; rewrite -> leEq_def; intro H0. cut ((y[-]x[/] _[//]pos_ap_zero _ _ Hy) [<=] [0]). intro H1. apply less_irreflexive_unfolded with (x := x). apply less_leEq_trans with y; auto. astepr (x[+][0]); apply shift_leEq_plus'. rstepl ((y[-]x[/] _[//]pos_ap_zero _ _ Hy) [*]y). apply shift_mult_leEq with (pos_ap_zero _ _ Hy); auto. rstepr ZeroR; auto. astepr (Log y Hy[-]Log x Hx). unfold Log in |- *; simpl in |- *. apply leEq_wdr with (Integral (prim_lemma _ _ log_defn_lemma x Hx y Hy)). 2: rstepl (Integral (prim_lemma _ _ log_defn_lemma [1] (pos_one _) x Hx) [+] Integral (prim_lemma _ _ log_defn_lemma x Hx y Hy) [-] Integral (prim_lemma _ _ log_defn_lemma [1] (pos_one _) x Hx)). 2: apply cg_minus_wd; algebra. 2: apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 [1] y x). 2: apply included_imp_Continuous with (openl [0]); [ apply log_defn_lemma | intros x0 H1; inversion_clear H1 ]. 2: simpl in |- *; apply less_leEq_trans with (Min (Min [1] y) x); auto; repeat apply less_Min; auto; apply pos_one. cut (Continuous_I (less_leEq _ _ _ H0) {1/}FId). intro H1. apply leEq_wdr with (integral _ _ _ _ H1). 2: apply eq_symmetric_unfolded; apply Integral_integral. rstepl (([1][/] _[//]pos_ap_zero _ _ Hy) [*] (y[-]x)). apply lb_integral. intros x0 H2 Hx0; simpl in |- *. elim H2; intros H3 H4; apply recip_resp_leEq; auto. apply less_leEq_trans with x; auto. apply included_imp_Continuous with (openl [0]); [ apply log_defn_lemma | red in |- *; intros x0 X ]. inversion_clear X; simpl in |- *; apply less_leEq_trans with x; auto. Qed.
imports: CoRN.transc.TaylorSeries