proposition: Lemma ex_series_DAlembert (a : nat -> R) (k : R) : k < 1 -> (forall n, a n <> 0) -> is_lim_seq (fun n => Rabs (a (S n) / a n)) k -> ex_series (fun n => Rabs (a n)).
proof: Proof. move => Hk Ha H. have : exists N, forall n, (N <= n)%nat -> Rabs (a (S n) / a n) <= (k+1)/2. apply is_lim_seq_spec in H. case: (fun He => H (mkposreal ((1-k)/2) He)). move: (fun He => is_pos_div_2 (mkposreal (1-k) He)) => /= He ; apply: He. by apply -> Rminus_lt_0. move => {H} /= Hk1 N H. exists N => n Hn. move: (H n Hn) => {} H. apply Rabs_lt_between' in H ; case: H => _ H ; field_simplify in H ; rewrite ?Rdiv_1 in H ; by apply Rlt_le. case => {H} N H. apply ex_series_incr_n with N. apply @ex_series_le with (fun n => Rabs (a N) * ((k+1)/2)^n). move => n. rewrite /norm /= /abs /= Rabs_Rabsolu. rewrite Rmult_comm ; apply Rle_div_l. by apply Rabs_pos_lt. rewrite -Rabs_div. elim: n => [ | n IH]. rewrite Nat.add_0_r /Rdiv Rinv_r. rewrite Rabs_R1 ; by apply Rle_refl. by apply Ha. replace (Rabs (a (N + S n)%nat / a N)) with (Rabs (a (S (N + n))/a (N+n)%nat) * Rabs (a (N + n)%nat / a N)). simpl ; apply Rmult_le_compat. by apply Rabs_pos. by apply Rabs_pos. apply H, Nat.le_add_r. by apply IH. rewrite -Rabs_mult ; apply f_equal. rewrite plus_n_Sm ; field ; split ; by apply Ha. by apply Ha. apply @ex_series_scal_l. set k0 := ((k + 1) / 2). exists (/(1-k0) * (1-k0*0)). apply filterlim_ext with (fun N => / (1 - k0) * (1 - k0 ^ S N)). move => n ; rewrite sum_n_Reals; rewrite tech3. by apply Rmult_comm. unfold k0 ; lra. apply (is_lim_seq_scal_l (fun N0 => (1 - k0 ^ S N0)) (/ (1 - k0)) (Finite (1-k0*0))). apply (is_lim_seq_minus _ _ (Finite 1) (Finite (k0*0))). by apply is_lim_seq_const. simpl pow ; apply (is_lim_seq_scal_l _ _ (Finite 0)). apply (is_lim_seq_geom k0). rewrite Rabs_pos_eq. unfold k0 ; lra. apply Rle_trans with (2 := H N (Nat.le_refl _)) ; by apply Rabs_pos. easy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy