proposition: Lemma CV_radius_Reals_0 (a : nat -> R) (r : posreal) : Rbar_lt (Finite r) (CV_radius a) -> CVN_r (fun n x => a n * x ^ n) r.
proof: Proof. move => Hr. rewrite /CVN_r /Boule. have H := CV_radius_bounded a. exists (fun n => Rabs (a n * r ^ n)). exists (Series (fun n => Rabs (a n * r ^ n))) ; split. rewrite -(Rabs_pos_eq r (Rlt_le _ _ (cond_pos r))) in Hr. apply CV_disk_inside in Hr. apply Lim_seq_correct' in Hr ; rewrite -/(Series (fun n : nat => Rabs (a n * r ^ n))) in Hr. move => e He. apply is_lim_seq_spec in Hr. case: (Hr (mkposreal e He)) => /= {Hr} N Hr. exists N => n Hn. replace (sum_f_R0 (fun k : nat => Rabs (Rabs (a k * r ^ k))) n) with (sum_f_R0 (fun k : nat => (Rabs (a k * r ^ k))) n). rewrite <- sum_n_Reals; by apply Hr. elim: n {Hn} => /= [ | n IH] ; rewrite Rabs_Rabsolu. by []. by rewrite IH. move => n x Hx. rewrite ?Rabs_mult -?RPow_abs. apply Rmult_le_compat_l. by apply Rabs_pos. apply pow_incr ; split. by apply Rabs_pos. rewrite (Rabs_pos_eq r). rewrite Rminus_0_r in Hx. by apply Rlt_le. by apply Rlt_le, r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series