proposition: Theorem ln_continue : forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y.
proof: Proof. intros y H. unfold continue_in, limit1_in, limit_in; intros eps Heps. assert (H1:1 < exp eps). { rewrite <- exp_0. apply exp_increasing; apply Heps. } assert (H2:exp (- eps) < 1). { apply Rmult_lt_reg_l with (exp eps). - apply exp_pos. - rewrite <- exp_plus; rewrite Rmult_1_r; rewrite Rplus_opp_r; rewrite exp_0; apply H1. } exists (Rmin (y * (exp eps - 1)) (y * (1 - exp (- eps)))); split. { red; apply Rmin_case; nra. } unfold dist, R_met, Rdist; simpl. intros x [[H3 H4] H5]. assert (Hxyy:y * (x * / y) = x). { field. lra. } replace (ln x - ln y) with (ln (x * / y)). 2:{ rewrite ln_mult;try apply Rinv_0_lt_compat; try assumption. rewrite ln_Rinv;try assumption. ring. } pose proof (Rinv_0_lt_compat y) as Hinvy. case (Rtotal_order x y); [ intros Hxy | intros [Hxy| Hxy] ]. - rewrite Rabs_left. 2:{ rewrite <- ln_1. apply ln_increasing;nra. } apply Ropp_lt_cancel; rewrite Ropp_involutive. apply exp_lt_inv. rewrite exp_ln. 2:nra. apply Rmult_lt_reg_l with (r := y). { apply H. } rewrite Hxyy. apply Ropp_lt_cancel. apply Rplus_lt_reg_l with (r := y). replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps))); [ idtac | ring ]. replace (y + - x) with (Rabs (x - y)). 2:{ rewrite Rabs_left; [ ring | idtac ]. lra. } apply Rlt_le_trans with (1 := H5); apply Rmin_r. - rewrite Hxy; rewrite Rinv_r. 2:lra. rewrite ln_1; rewrite Rabs_R0; apply Heps. - rewrite Rabs_right. 2:{ rewrite <- ln_1. apply Rgt_ge; red; apply ln_increasing;nra. } apply exp_lt_inv. rewrite exp_ln. 2:nra. apply Rmult_lt_reg_l with (r := y). { apply H. } rewrite Hxyy. apply Rplus_lt_reg_l with (r := - y). replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ]. replace (- y + x) with (Rabs (x - y)). 2:{ rewrite Rabs_right; [ ring | idtac ]. lra. } apply Rlt_le_trans with (1 := H5); apply Rmin_l. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra