proposition: Lemma Rpser_little_O_partial_sum : forall N (H : 0 < r) (Hcv : Rseq_cv En 0) (pr : Cv_radius_weak Un r), (fun p => weaksum_r Un r pr (En p) - sum_f_R0 (fun n => Un n * (En p) ^ n) N) = o((fun p => (En p) ^ N)).
proof: Proof. intros N H Hcv pr. eapply Rseq_big_O_little_O_trans; [apply Rpser_big_O_partial_sum; assumption|]. intros eps Heps. destruct (Hcv eps Heps) as [M HM]. exists M; intros n Hn. simpl pow; rewrite Rabs_mult. apply Rmult_le_compat_r; [apply Rabs_pos|]. apply Rlt_le; replace (En n) with (En n - 0) by field. apply HM; assumption. Qed.
imports: Reals Lra Rsequence Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpser_derivative