proposition: Lemma CV_radius_infinite_DAlembert (a : nat -> R) : (forall n:nat, a n <> 0) -> is_lim_seq (fun n:nat => Rabs (a (S n) / a n)) 0 -> CV_radius a = p_infty.
proof: Proof. move => Ha Hda. rewrite /CV_radius /Lub_Rbar ; case: ex_lub_Rbar ; case => [cv | | ] //= [ub lub] ; have : False => //. have H : CV_disk a (cv + 1). have H : 0 < cv + 1. apply Rlt_le_trans with (0+1). rewrite Rplus_0_l ; by apply Rlt_0_1. apply Rplus_le_compat_r. apply ub. exists (Rabs (a O)). apply (is_lim_seq_ext (fun _ => Rabs (a O)) _ (Rabs (a 0%nat))). elim => [ | k IH] /=. by rewrite sum_O Rmult_1_r. by rewrite sum_Sn /= Rmult_0_l Rmult_0_r Rabs_R0 /plus /= Rplus_0_r. by apply is_lim_seq_const. apply ex_series_DAlembert with 0. by apply Rlt_0_1. move => n ; apply Rmult_integral_contrapositive_currified. by[]. by apply Rgt_not_eq, pow_lt. rewrite -(Rmult_0_r (Rabs (cv + 1))). apply (CV_disk_DAlembert_aux a (cv + 1)). by apply Rgt_not_eq. by []. by []. move: (ub (cv+1) H). by apply Rbar_lt_not_le, Rlt_n_Sn. case: (ub 0) => //. exists (Rabs (a O)). apply (is_lim_seq_ext (fun _ => Rabs (a O)) _ (Rabs (a 0%nat))). elim => [ | k IH] /=. by rewrite sum_O Rmult_1_r. by rewrite sum_Sn /= Rmult_0_l Rmult_0_r Rabs_R0 /plus /= Rplus_0_r. by apply is_lim_seq_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series