proposition: Lemma Rpser_infinite_cv_radius_caracterization : forall An, (forall x, {l | Rpser An x l}) -> infinite_cv_radius An.
proof: Proof. intros An weaksum r ; destruct (weaksum r) as (l, Hl) ; apply Rpser_bound_criteria 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