proposition: Lemma ln_minus_finite_cv_radius : finite_cv_radius Un 1.
proof: Proof. assert (Un_decr : Un_decreasing (- (fun n => Un (S n)))%Rseq). assert (Hrew : forall n, Un (S n) = -/ INR (S n)). intro ; reflexivity. intro n ; unfold Rseq_opp ; repeat rewrite Hrew, Ropp_involutive. apply Rle_Rinv ; intuition. assert (Un_cv_0 : Un_cv (fun n : nat => - Un (S n)) 0). replace (fun n : nat => Un (S n)) with (fun n => - / INR (S n)). rewrite <- Ropp_involutive ; do 2 apply Rseq_cv_opp_compat. apply Rseq_cv_pos_infty_inv_compat. intro M. assert (lt_0_1 : (0 < 1)%nat) by auto ; destruct (Rseq_poly_cv 1 lt_0_1 M) as [N HN] ; exists N ; intros n n_gt_N ; apply Rlt_trans with (INR n). rewrite <- pow_1 ; apply HN ; assumption. intuition. reflexivity. destruct (alternated_series (fun n => - Un (S n)) Un_decr Un_cv_0) as [l Hl]. rewrite <- Rabs_R1. rewrite <- Rabs_Ropp. apply Rpser_finite_cv_radius_caracterization with l. unfold Pser, infinite_sum. intros eps eps_pos ; destruct (Hl eps eps_pos) as [N HN] ; exists (S N) ; intros n n_lb ; unfold R_dist. rewrite <- Rabs_Ropp. rewrite Ropp_minus_distr. assert (Hrew := (Rseq_pps_opp_compat Un (-1) n)) ; unfold Rseq_opp in Hrew ; unfold Rminus . change (-(1)) with (-1). rewrite <- Hrew. apply Rle_lt_trans with (R_dist (sum_f_R0 (tg_alt (fun n0 : nat => - Un (S n0))) (pred n)) l). right ; rewrite <- Rabs_Ropp ; unfold R_dist ; apply Rabs_eq_compat. clear - n_lb; induction n ; unfold tg_alt. inversion n_lb. simpl pred. clear ; induction n. compute ; field. unfold Rseq_pps, Rseq_sum in *. rewrite tech5. repeat rewrite Ropp_plus_distr in *. rewrite <- Rplus_assoc. rewrite IHn. unfold Rminus ; rewrite tech5. repeat rewrite Rplus_assoc ; apply Rplus_eq_compat_l. rewrite Rplus_comm ; apply Rplus_eq_compat_r. unfold gt_pser. unfold Rseq_mult. simpl pow. ring. apply HN ; intuition. intros M Hconv. unfold Rpser_abs in *. pose (fun n => match n with O => 0 | S _ => / INR n end) as An. apply Rseq_cv_not_infty with (sum_f_R0 An); split. exists M. refine (proj1 (Rser_cv_ext _ An M _) Hconv). intros [|n]. simpl. unfold gt_abs_pser. unfold Rseq_abs. unfold gt_pser. unfold Rseq_mult. simpl. rewrite Rmult_0_l. rewrite Rabs_R0. reflexivity. unfold Un, An. unfold gt_abs_pser. unfold Rseq_abs. unfold gt_pser. unfold Rseq_mult. rewrite Rabs_mult. rewrite pow_1_abs. rewrite Rabs_Ropp. rewrite Rabs_pos_eq; [ | apply Rlt_le; apply Rinv_0_lt_compat; INR_solve]. ring. apply Rseq_cv_pos_infty_shift_compat. eapply Rseq_cv_pos_infty_eq_compat. 2:eapply Rseq_equiv_cv_pos_infty_compat. 2:apply Rseq_equiv_sym. 2:apply harmonic_series_equiv. intro n; unfold Rseq_shift. induction n. simpl; ring. rewrite tech5. rewrite IHn. reflexivity. apply Rseq_subseq_cv_pos_infty_compat with (fun n => ln (INR n)). exists (exist _ _ (extractor_Rseq_iter_S 2)). unfold extracted, is_extractor. reflexivity. apply Rseq_ln_cv. 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