proposition: Lemma Rser_RiemannInt_cv_pos_infty : exists pr : forall (n : nat), Riemann_integrable f 0 (INR n), Rseq_cv_pos_infty (fun n => RiemannInt (pr (S n))) -> (sum_f_R0 (fun n => f (INR n))) ~ (fun n => RiemannInt (pr (S n))).
proof: Proof. assert (pr : forall n : nat, Riemann_integrable f 0 n). intro n. apply continuity_implies_RiemannInt. intuition. intros x [Hx _]; apply (Hcont x Hx). exists pr. intro Hdiv. destruct Rser_RiemannInt_link as [ l Hl]. apply Rseq_equiv_sym. unfold Rseq_equiv, Rseq_minus. apply Rseq_cv_little_O_cv_pos_infty with (-l). apply Rseq_cv_eq_compat with (sum_f_R0 (fun n : nat =>- (f (INR n) - RiemannInt (Riemann_integrable_f_n_Sn n)))). intro n. destruct (Rint_generalized_Chasles f (fun n =>RiemannInt (Riemann_integrable_f_n_Sn n)) (fun n => Rint_RiemannInt_link f n (S n) (Riemann_integrable_f_n_Sn n)) n) as [prn H]. rewrite RiemannInt_P5 with _ _ _ (pr (S n)) prn. rewrite H. rewrite <- minus_sum. apply sum_eq; intros p Hp. unfold Rminus. ring. unfold Rser_cv in Hl. apply Rser_cv_opp_compat; apply Hl. apply Hdiv. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral