proposition: Lemma ln_minus_taylor_sum : forall x, Rabs x < 1 -> sum x = (ln (1 - x)).
proof: Proof. intros x Hx. pose (f := comp ln (fct_cte 1 - id)). pose (df := fun u => / (1 - u) * (0 - 1)). assert (Hb : forall u, Rmin 0 x <= u <= Rmax 0 x -> -1 < u < 1). destruct (Rabs_def2 x 1 Hx) as [Hmax Hmin]. intros u [Hul Hur]. unfold Rmin, Rmax in Hul, Hur. destruct Rle_dec; split; lra. pose (Hcv := ln_minus_cv_radius). pose (g := weaksum_r Un 1 Hcv). pose (dg := weaksum_r_derive Un 1 Hcv). destruct Rint_derive2 with (f := f) (a := 0) (b := x) (d := df) as [pr HI]. intros u Hu. apply derivable_pt_lim_comp. apply derivable_pt_lim_minus. apply derivable_pt_lim_const. apply derivable_pt_lim_id. apply derivable_pt_lim_ln. apply Rgt_minus; apply (Hb u Hu). intros u Hu. apply continuity_pt_mult. apply continuity_pt_inv. apply continuity_pt_minus. apply continuity_pt_const; unfold constant; auto. apply derivable_continuous_pt; apply derivable_pt_id. apply Rgt_not_eq; apply Rgt_minus; apply (Hb u Hu). apply continuity_pt_minus. apply continuity_pt_const; unfold constant; auto. apply continuity_pt_const; unfold constant; auto. assert (Heq : forall u, -1 < u < 1 -> dg u = df u). intros u [Hul Hur]; unfold df, dg. replace (/ (1 - u) * (0 - 1)) with (- / (1 - u)) by (field; intros Hc; lra). assert (Habs : Rabs u < 1). unfold Rabs; destruct Rcase_abs; lra. assert (Hser1 := weaksum_r_derive_sums Un 1 Hcv u Habs). assert (Hser2 := GP_infinite u Habs). eapply Rseq_cv_unique. apply Hser1. assert (Hrw : - sum_f_R0 (fun n => 1 * u ^ n) == sum_f_R0 (fun n => An_deriv Un n * u ^ n)). unfold An_deriv. unfold Rseq_opp; intros n; induction n. simpl; unfold Rseq_shift, Rseq_mult; simpl; field. simpl sum_f_R0 at 1; rewrite Ropp_plus_distr. rewrite IHn. simpl; apply Rplus_eq_compat_l; destruct n. simpl. unfold Rseq_shift, Rseq_mult; simpl; field. unfold Rseq_shift. unfold Rseq_mult. unfold Un. field; assert (H := pos_INR (S n)); intros Hc. do 2 rewrite S_INR in Hc. lra. eapply Rseq_cv_eq_compat; unfold Rseq_pps, Rseq_sum, gt_pser. erewrite <- Hrw. reflexivity. apply Rseq_cv_opp_compat; apply Hser2. edestruct Rint_eq_compat with (f := df) (g := dg) (a := 0) (b := x) as [pr2 HI2]. intros u Hu. apply Heq; apply Hb; assumption. exists pr; apply HI. destruct Rint_derive2 with (f := g) (a := 0) (b := x) (d := dg) as [pr3 HI3]. intros u Hu. apply derivable_pt_lim_weaksum_r. apply Hb in Hu. destruct Hu as [Hul Hur]. unfold Rabs; destruct Rcase_abs; lra. intros u Hu. assert (Hu2 := Hb u Hu). destruct Hu2 as [Hul Hur]. assert (Hct : continuity_pt df u). unfold df. apply continuity_pt_mult. apply continuity_pt_inv; [|intros Hc; lra]. apply continuity_pt_minus. apply continuity_pt_const; unfold constant; auto. apply derivable_continuous_pt; apply derivable_pt_id. apply continuity_pt_const; unfold constant; auto. eapply continuity_pt_eq_compat; [|apply Hct]. pose (alp1 := u / 2 + / 2). pose (alp2 := /2 - u / 2). exists (Rmin alp1 alp2); split. apply Rmin_pos_lt. unfold alp1; lra. unfold alp2; lra. intros y Hy; symmetry. apply Heq. unfold alp1, alp2, R_dist, Rabs, Rmin in *. destruct Rcase_abs as [Hc|Hc] in Hy; destruct Rle_dec as [Hl|Hl] in Hy; split; try lra; try apply Rnot_le_lt in Hl; lra. assert (Hint : Rint dg 0 x (f x - f 0)). apply Rint_eq_compat with (f := df). intros u Hu. apply Heq; apply Hb; assumption. exists pr; assumption. assert (Heq_fun : g x - g 0 = f x - f 0). eapply Rint_uniqueness. exists pr3; assumption. assumption. replace (ln (1 - x)) with (weaksum_r Un 1 Hcv x). unfold sum, Hcv; reflexivity. unfold f, g, comp, fct_cte, id, minus_fct in Heq_fun; hnf in Heq_fun. replace (1 - 0) with 1 in Heq_fun by ring; rewrite ln_1 in Heq_fun. rewrite Rminus_0_r in Heq_fun. replace (weaksum_r Un 1 Hcv 0) with 0 in Heq_fun. rewrite Rminus_0_r in Heq_fun; assumption. symmetry. eapply Rseq_cv_unique. apply weaksum_r_sums; rewrite Rabs_R0; lra. intros eps Heps; exists 0%nat; intros n _. unfold Rseq_pps, gt_pser. rewrite sum_eq_R0. rewrite R_dist_eq; assumption. intros m _; unfold Un; destruct m. unfold Rseq_mult. field. unfold Rseq_mult. rewrite pow_ne_zero; [field|]. apply not_0_INR; auto. auto. Qed.
imports: Reals MyReals Rsequence_def Rsequence_facts Rsequence_sums_facts Rseries_def Rpser_def Rpser_sums Rpser_sums_facts Rpser_derivative Rpser_radius_facts Rpser_taylor Lra Rintegral Rseries_facts Rseries_RiemannInt Rsequence_subsequence Rtactic