proposition: Lemma Rser_big_O_maj : forall (Un Vn: Rseq), (forall n : nat, 0 <= Vn n) -> Un = O (Vn) -> exists K, exists SN, 0 <= K /\ forall n : nat, Rseq_sum (|Un|) n <= K* (Rseq_sum Vn n) + SN.
proof: Proof. intros Un Vn Vn_pos [K [HK [N HN]]] ; apply Rge_le in HK ; exists K ; exists (Rseq_sum (| Un |) N) ; split ; [assumption |]. intro n ; destruct (le_lt_dec n N) as [HnN | HNn]. transitivity (Rseq_sum (| Un |) N). destruct (eq_nat_dec n N) as [Heq | Hneq]. subst ; reflexivity. unfold Rseq_sum ; rewrite tech2 with (| Un |) n N ; [| lia] ; apply Rplus_le_simpl_l, Rseq_sum_pos ; intros ; apply Rabs_pos. apply Rplus_le_simpl_r, Rmult_le_pos, Rseq_sum_pos ; assumption. unfold Rseq_sum ; rewrite tech2 with (|Un|) N n, Rplus_comm. apply Rplus_le_compat_r ; rewrite tech2 with Vn N n, Rmult_plus_distr_l. transitivity ((K * Rseq_sum (Rseq_shifts Vn (S N)))%Rseq (n - S N)%nat). rewrite <- Rseq_sum_scal_compat_l ; apply Rseq_sum_le_compat ; unfold Rseq_shifts, Rseq_abs, Rseq_mult, Rseq_constant ; intros ; rewrite <- (Rabs_right (Vn _)), HN. reflexivity. lia. apply Rle_ge ; apply Vn_pos. apply Rplus_le_simpl_r, Rmult_le_pos, Rseq_sum_pos, Vn_pos. assumption. assumption. assumption. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq