proposition: Lemma Rpser_finite_cv_radius_caracterization : forall An x l, Rpser An x l -> (forall l : R, ~ Rpser_abs An x l) -> finite_cv_radius An (Rabs x).
proof: Proof. intros An x l Hcv Hncv ; split; intros r Hr. apply Cv_radius_weak_le_compat with x. rewrite Rabs_pos_eq ; [left |] ; apply Hr. apply (Rpser_bound_criteria _ _ l Hcv). intro Hf ; destruct (Rpser_abs_cv_radius_weak An r Hf x Hr) as [l' Hl'] ; apply Hncv with l' ; 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