proposition: Lemma Alembert_C2 : forall An:nat -> R, (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
proof: Proof. intros. set (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2). set (Wn := fun i:nat => (2 * Rabs (An i) - An i) / 2). assert (forall n:nat, 0 < Vn n). { apply Alembert_C2_aux_positivity;assumption. } assert (Wn_aux : Wn = fun i => (2 * Rabs (- An i) + (- An i)) / 2). { apply FunctionalExtensionality.functional_extensionality. intros n. unfold Wn,Rminus. do 3 f_equal. symmetry;apply Rabs_Ropp. } assert (forall n:nat, 0 < Wn n). { rewrite Wn_aux. apply Alembert_C2_aux_positivity. intros;apply Ropp_neq_0_compat, H. } assert (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0). { apply Alembert_C2_aux_Un_cv;assumption. } assert (Un_cv (fun n:nat => Rabs (Wn (S n) / Wn n)) 0). { rewrite Wn_aux. apply (Alembert_C2_aux_Un_cv (fun n => - An n)). - intros;apply Ropp_neq_0_compat, H. - replace (fun n : nat => Rabs (- An (S n) / - An n)) with (fun n : nat => Rabs (An (S n) / An n));[assumption|]. apply FunctionalExtensionality.functional_extensionality. intros n. f_equal. field;trivial. } pose proof (Alembert_C1 Vn H1 H3) as (x,p). pose proof (Alembert_C1 Wn H2 H4) as (x0,p0). exists (x - x0); unfold Un_cv; unfold Un_cv in p; unfold Un_cv in p0; intros; assert (H6:0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. } destruct (p (eps / 2) H6) as (x1,H8). clear p. destruct (p0 (eps / 2) H6) as (x2,H9). clear p0. set (N := max x1 x2). exists N; intros; replace (sum_f_R0 An n) with (sum_f_R0 Vn n - sum_f_R0 Wn n). 2:{ symmetry ; apply tech11; intro; unfold Vn, Wn; unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_eq_reg_l with 2. - rewrite Rmult_minus_distr_l; repeat rewrite <- Rmult_assoc; rewrite Rinv_r. + ring. + discrR. - discrR. } unfold Rdist; replace (sum_f_R0 Vn n - sum_f_R0 Wn n - (x - x0)) with (sum_f_R0 Vn n - x + - (sum_f_R0 Wn n - x0)) by ring; apply Rle_lt_trans with (Rabs (sum_f_R0 Vn n - x) + Rabs (- (sum_f_R0 Wn n - x0))). { apply Rabs_triang. } rewrite Rabs_Ropp; apply Rlt_le_trans with (eps / 2 + eps / 2). + apply Rplus_lt_compat. * unfold Rdist in H8; apply H8; unfold ge; apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_l | assumption ]. * unfold Rdist in H9; apply H9; unfold ge; apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_r | assumption ]. + right; apply Rplus_half_diag. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra