proposition: Lemma Rpser_abel2 : forall An r, Cv_radius_weak An r -> forall r' : posreal, r' < r -> CVN_r (fun n x => gt_pser An x n) r'.
proof: Proof. intros An r Pr [a a_pos] r'_ub. assert (a_bd : Rabs a < r) by (rewrite Rabs_pos_eq ; [| left] ; assumption). assert (r_pos : 0 < r) by (apply Rlt_trans with a ; assumption). assert (r'_bd : Rabs (middle a r) < r). rewrite Rabs_pos_eq ; [apply middle_is_in_the_middle | left ; apply middle_lt_lt_pos_lt] ; assumption. rewrite Cv_radius_weak_abs in Pr. exists (gt_abs_pser An (middle a r)) ; exists (weaksum_r (| An |) r Pr (Rabs (middle a r))) ; split. rewrite <- Rseq_cv_Un_cv_equiv ; apply Rseq_cv_eq_compat with (Rseq_sum (gt_abs_pser An (middle a r))). intro n ; fold (Rseq_abs (gt_abs_pser An (middle a r))) ; apply Rseq_sum_ext with (Vn := gt_abs_pser An (middle a r)) ; apply Rseq_abs_idempotent. assert (tmp := Rseq_sum_ext _ _ (gt_abs_pser_unfold An (middle a r))) ; symmetry in tmp ; apply (Rseq_cv_eq_compat _ _ _ tmp) ; clear tmp. apply weaksum_r_sums ; rewrite Rabs_Rabsolu ; assumption. intros n y B ; apply gt_abs_pser_le_compat ; unfold Boule in B ; apply Rle_trans with a ; [left |]. unfold Rminus in B ; rewrite Ropp_0, Rplus_0_r in B ; apply B. rewrite Rabs_pos_eq ; [left ; apply middle_is_in_the_middle | left ; apply middle_lt_lt_pos_lt] ; assumption. Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR