proposition: Lemma Rpser_bound_criteria : forall (An : nat -> R) (x l : R), Rpser An x l -> Cv_radius_weak An x.
proof: Proof. intros An x l Hxl. destruct (Hxl 1) as [N HN] ; [lra |] ; unfold R_dist in HN. assert (H1: forall n, (S N <= n)%nat -> gt_abs_pser An x n <= Rmax 2 (Rabs (An O))). intros n n_lb ; destruct n ; unfold gt_abs_pser, Rseq_abs. unfold gt_pser, Rseq_mult ; simpl ; rewrite Rmult_1_r ; apply RmaxLess2. transitivity (Rabs ((Rseq_pps An x (S n) - l) - (Rseq_pps An x n - l))). right ; rewrite Rseq_pps_simpl ; apply Rabs_eq_compat ; unfold gt_pser, Rseq_mult ; ring. transitivity (Rabs (Rseq_pps An x (S n) - l) + Rabs (- (Rseq_pps An x n - l))). apply Rabs_triang. transitivity 2 ; [| apply RmaxLess1] ; rewrite Rabs_Ropp. apply Rplus_le_compat ; left ; apply HN ; lia. destruct (Rseq_partial_bound (gt_pser An x) (S N)) as (B,HB). exists (Rmax B (Rmax 2 (Rabs (An O)))). intros y [i Hi] ; subst ; destruct (le_lt_dec i (S N)) as [Hi_b | Hi_b]. apply Rle_trans with B ; [apply HB | apply RmaxLess1] ; intuition. apply Rle_trans with (Rmax 2 (Rabs (An O))) ; [apply H1 | apply RmaxLess2] ; intuition (auto with arith). Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics