proposition: Lemma ln1p_ln1pc : forall x, ln (1 + x) = (x * ln1pc x)%R.
proof: Proof. intros x. unfold ln1pc. destruct ln1pc_in_int as [Hx|Hx]. 2: field ; contradict Hx ; rewrite Hx ; split ; [ apply Rle_refl | apply Rlt_0_1 ]. destruct ln1pc_exists as [y Hy]. simpl. replace y with (PSeries (fun n => (-1)^n / INR (n + 1)) x). rewrite <- PSeries_incr_1. replace (ln (1 + x)) with (RInt (fun t => / (1 + t)) 0 x). rewrite <- (PSeries_ext (PS_Int (fun n => (-1)^n))). assert (Hc: Rbar_lt (Rabs x) (CV_radius (fun n : nat => (-1) ^ n))). rewrite (CV_radius_finite_DAlembert _ 1). now rewrite Rinv_1, Rabs_pos_eq. intros n. apply pow_nonzero. now apply IZR_neq. exact Rlt_0_1. apply is_lim_seq_ext with (fun _ => 1%R). intros n. change ((-1)^(S n) / (-1)^n)%R with (-(1) * (-1)^n */ (-1)^n)%R. rewrite Rmult_assoc, Rinv_r, Rmult_1_r, Rabs_Ropp. apply eq_sym, Rabs_R1. apply pow_nonzero. now apply IZR_neq. apply is_lim_seq_const. rewrite <- RInt_PSeries with (1 := Hc). apply RInt_ext. intros t. rewrite Rmin_left, Rmax_right by easy. intros Ht. rewrite <- (Ropp_involutive t) at 1. unfold PSeries. rewrite <- (Series_ext (fun k => (-t)^k)). apply eq_sym, Series_geom. rewrite Rabs_Ropp, Rabs_pos_eq. now apply Rlt_trans with x. now apply Rlt_le. intros n. replace (-t)%R with (-1 * t)%R by ring. apply Rpow_mult_distr. intros [|n]. easy. unfold PS_incr_1. now rewrite Nat.add_comm. apply is_RInt_unique. assert (H: forall t, -1 < t -> is_derive (fun t : R => ln (1 + t)) t (/ (1 + t))). intros t Ht. auto_derive. rewrite <- (Rplus_opp_r 1). now apply Rplus_lt_compat_l. apply Rmult_1_l. apply (is_RInt_ext (Derive (fun t => ln (1 + t)))). intros t. rewrite Rmin_left by easy. intros [Ht _]. apply is_derive_unique. apply H. apply Rlt_trans with (2 := Ht). now apply IZR_lt. replace (ln (1 + x)) with (ln (1 + x) - ln (1 + 0))%R. apply (is_RInt_derive (fun t => ln (1 + t))). intros t. rewrite Rmin_left by easy. intros [Ht _]. apply Derive_correct. eexists. apply H. apply Rlt_le_trans with (2 := Ht). now apply IZR_lt. intros t. rewrite Rmin_left by easy. intros [Ht _]. apply continuous_ext_loc with (fun t : R => /(1 + t)). apply locally_interval with (-1)%R p_infty. apply Rlt_le_trans with (2 := Ht). now apply IZR_lt. easy. clear t Ht. intros t Ht _. apply sym_eq, is_derive_unique. now apply H. apply continuous_comp. apply (continuous_plus (fun t : R => 1)). apply filterlim_const. apply filterlim_id. apply (filterlim_Rbar_inv (1 + t)). apply Rbar_finite_neq. apply Rgt_not_eq. rewrite <- (Rplus_0_l 0). apply Rplus_lt_le_compat with (1 := Rlt_0_1) (2 := Ht). rewrite Rplus_0_r, ln_1. apply Rminus_0_r. apply is_pseries_unique. apply is_lim_seq_Reals. apply Un_cv_ext with (2 := Hy). intros n. rewrite <- sum_n_Reals. apply sum_n_ext. intros m. rewrite pow_n_pow. unfold tg_alt. rewrite <- Rmult_assoc. apply Rmult_comm. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot