proposition: Lemma Rser_little_O_maj : forall (Un Vn : nat -> R), (forall n : nat, 0 <= Vn n) -> Un = o (Vn) -> forall eps, 0< eps -> exists SN, forall n : nat, sum_f_R0 (|Un|) n <= eps* (sum_f_R0 Vn n) + SN.
proof: Proof. intros Un Vn Vn_pos HO eps Heps. assert (0<= eps) as Heps_pos. apply Rlt_le; apply Heps. destruct (HO eps Heps) as [N HN]. exists (sum_f_R0 (|Un|) N). intro n; case (le_lt_dec n N); intro Hn. apply Rle_trans with (sum_f_R0 (|Un|) N). assert (n = N \/ n < N)%nat. lia. case H ; intro HnN. rewrite HnN; apply Rle_refl. rewrite tech2 with (|Un|) n N. apply Rplus_le_simpl_l. apply cond_pos_sum. intro k; apply Rabs_pos. apply HnN. apply Rplus_le_simpl_r. apply Rmult_le_pos; [apply Heps_pos | apply cond_pos_sum; apply Vn_pos]. rewrite tech2 with (|Un|) N n. rewrite Rplus_comm. apply Rplus_le_compat_r. rewrite tech2 with Vn N n. rewrite Rmult_plus_distr_l. apply Rle_trans with (eps * sum_f_R0 (fun i : nat => Vn (S N + i)%nat) (n- (S N)))%R. rewrite scal_sum. apply sum_Rle. intros n0 Hn0. rewrite <- Rabs_pos_eq. rewrite Rmult_comm; rewrite Rabs_mult. rewrite Rabs_pos_eq with eps. apply HN; lia. apply Heps_pos. apply Rmult_le_pos; [apply Vn_pos | apply Heps_pos]. apply Rplus_le_simpl_r. apply Rmult_le_pos; [apply Heps_pos | apply cond_pos_sum; apply Vn_pos]. apply Hn. apply Hn. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq