proposition: Lemma Cpser_finite_cv_radius_caracterization : forall (An : nat -> C) (z l : C), Cpser An z l -> (forall l' : R, ~ Cpser_norm An z l') -> finite_cv_radius An (Cnorm z).
proof: Proof. intros An z l Hcv Hncv. split; intros x Hx. apply Cv_radius_weak_le_compat with (Cnorm z). rewrite Rabs_Cnorm ; rewrite Rabs_right ; intuition. apply (Cpser_bound_criteria _ _ l Hcv). intro Hf. destruct (Cpser_abel2_prelim An x Hf z) as [l' Hl']. assumption. apply (Hncv (Cnorm l')). Abort. Lemma Cpser_infinite_cv_radius_caracterization : forall An, (forall x, {l | Cpser An x l}) -> infinite_cv_radius An. Proof. intros An weaksum r ; destruct (weaksum r) as (l, Hl). assert (H := Cpser_bound_criteria An r l Hl). rewrite Cnorm_IRC_Rabs in H. apply Cv_radius_weak_le_compat with (Rabs r). rewrite Rabs_Rabsolu ; right ; reflexivity. assumption. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts