proposition: Lemma ln_taylor_3 : Sn = O(Qn 4).
proof: Proof. unfold Sn, Rn in *. eapply Rseq_big_O_asymptotic. intros; eassumption. exists 2%nat. eapply Rseq_big_O_eq_compat. 3: eapply Rpser_big_O_partial_sum with (Un := Tn) (pr := ln_plus_cv_radius) (En := fun n => / INR (2 + n)) (N := 3%nat). intros n ; unfold Rseq_shifts. rewrite <- ln_plus_taylor_sum. unfold Tn; apply Rplus_eq_compat_l. unfold Rseq_pps. unfold Rseq_sum. unfold gt_pser. unfold Rseq_mult. simpl; destruct n; simpl; field. destruct n; intros Hc. lra. assert (H := pos_INR (S n)); lra. rewrite Rabs_Rinv. rewrite <- Rinv_1. apply Rinv_1_lt_contravar; [apply Rle_refl|]. rewrite Rabs_right; [|apply Rle_ge; apply pos_INR]. replace (2 + n)%nat with (S (S n)) by lia. repeat rewrite S_INR. assert (H := pos_INR n); lra. replace (2 + n)%nat with (S (S n)) by lia. repeat rewrite S_INR. intros Hc; assert (H := pos_INR n); lra. apply Rseq_eq_refl. lra. apply Rseq_cv_pos_infty_inv_compat. apply Rseq_cv_pos_infty_eq_compat with (Un := fun n => 2 + Rseq_poly 1 n). intros n; replace (2 + n)%nat with (S (S n)) by lia. do 2 rewrite S_INR; unfold Rseq_poly; ring. eapply Rseq_cv_finite_plus_pos_infty_r. apply Rseq_constant_cv. apply Rseq_poly_cv; auto. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis