proposition: Lemma Rseq_equiv_ln : forall Un, Rseq_cv Un 0 -> (fun n => ln (1 + Un n)) ~ Un.
proof: Proof. intros Un Hu. destruct (Hu 1) as [M HM]; [lra|]. apply Rseq_equiv_sym. intros eps Heps. assert (H1 : 0 < 1) by lra. destruct (Rpser_little_O_partial_sum _ Un 1 1 H1 Hu ln_plus_cv_radius eps Heps) as [N HN]. exists (Nat.max M N); intros n Hn. unfold Rseq_minus; simpl. pattern Un at 2; replace (Un n) with (Un n ^ 1) by field. eapply Rle_trans; [right|apply HN]. simpl; rewrite ln_plus_taylor_sum. rewrite Rabs_minus_sym. apply f_equal; field. replace (Un n) with (Un n - 0) by field; apply HM. eapply Nat.le_trans; [apply Nat.le_max_l|eassumption]. eapply Nat.le_trans; [apply Nat.le_max_r|eassumption]. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics