proposition: Lemma Rseq_cv_pos_infty_criteria : forall An d, 0 < d -> (forall n, 0 <= An n) -> (forall M, exists N, (N >= M)%nat /\ d <= Rseq_sum (Rseq_shifts An M) (N - M)) -> Rseq_cv_pos_infty (Rseq_sum An).
proof: Proof. intros An d d_pos An_pos HAn. assert (HAn' : forall M, exists N, forall n, (N < n)%nat -> INR M * d <= Rseq_sum An n). intro M ; induction M. destruct (HAn O) as [N [_ HN]] ; exists N. intros n n_lb ; simpl ; rewrite Rmult_0_l. rewrite (Rseq_sum_split_compat _ _ _ n_lb) ; apply Rplus_le_le_0_compat. transitivity d. left ; assumption. rewrite <- (Nat.sub_0_r N) ; erewrite Rseq_sum_ext ; [| symmetry ; eapply Rseq_shifts_0 ] ; assumption. apply Rseq_sum_pos ; intros ; apply An_pos. destruct IHM as [N HN] ; destruct (HAn (S (S N))) as [N' [N'_lb HN']] ; exists N' ; assert (N'_lb' : (S N < N')%nat) by lia. intros n n_lb ; rewrite S_INR, Rmult_plus_distr_r, Rmult_1_l, (Rseq_sum_split_compat _ _ _ n_lb), (Rseq_sum_split_compat _ _ _ N'_lb'), Rplus_assoc. apply Rplus_le_compat. apply HN ; auto. rewrite <- (Rplus_0_r d) ; apply Rplus_le_compat. apply HN'. apply Rseq_sum_pos ; intros ; apply An_pos. intro B ; pose (M := up (Rabs B / d)) ; destruct (archimed (Rabs B / d)) as [HB _]. assert (M_pos : (0 <= M)%Z). apply le_IZR ; simpl ; eapply Rle_trans ; [| left ; eassumption]. apply Rle_mult_inv_pos ; [apply Rabs_pos | assumption]. destruct (IZN _ M_pos) as [M' HM'] ; destruct (HAn' M') as [N HN] ; exists (S N) ; intros n n_lb. apply Rlt_le_trans with (INR M' * d)%R ; [| apply HN ; lia]. apply Rle_lt_trans with (Rabs B) ; [apply Rle_abs |]. rewrite <- (Rmult_1_r (Rabs B)), <- (Rinv_l d), <- Rmult_assoc, INR_IZR_INZ, <- HM'. apply Rmult_lt_compat_r ; [assumption | apply HB]. apply Rgt_not_eq ; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra