proposition: Lemma Rser_big_O_cv_weak : forall (Un Vn : nat -> R), (forall n : nat, 0 <= Un n) -> (forall n : nat, 0 <= Vn n) -> Un = O(Vn) -> {lv | Rser_cv Vn lv} -> {lu | Rser_cv Un lu}.
proof: Proof. intros Un Vn Un_pos Vn_pos HO Hlv; destruct Hlv as [lv Hlv]. assert ({M | Rser_bound_max Un M}) as HM. assert ({M : R | is_lub (EUn (sum_f_R0 Un))M})as HMub. apply ub_to_lub. destruct (Rser_big_O_maj Un Vn Vn_pos HO) as [K [SN [K_pos Hmaj]]]. exists (K*lv+SN)%R. intros x Hx; destruct Hx as [n Hn]; rewrite Hn. apply Rle_trans with (K * sum_f_R0 Vn n + SN)%R. rewrite (sum_eq Un (fun k => Rabs (Un k))). apply Hmaj. intros i Hi; rewrite Rabs_pos_eq; [reflexivity | apply Un_pos]. apply Rplus_le_compat_r. apply Rmult_le_compat_l. apply K_pos. apply growing_ineq. apply Rser_pos_growing; apply Vn_pos. apply Hlv. destruct HMub as [M [HM _]]; exists M. intro n; apply HM. exists n; reflexivity. destruct HM as [M HM]. apply Rser_pos_bound_cv with M. apply Un_pos. apply HM. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq