proposition: Lemma cauchy_abs : forall An:nat -> R, Cauchy_crit_series (fun i:nat => Rabs (An i)) -> Cauchy_crit_series An.
proof: Proof. unfold Cauchy_crit_series; unfold Cauchy_crit. intros. elim (H eps H0); intros. exists x. intros. cut (Rdist (sum_f_R0 An n) (sum_f_R0 An m) <= Rdist (sum_f_R0 (fun i:nat => Rabs (An i)) n) (sum_f_R0 (fun i:nat => Rabs (An i)) m)). - intro. apply Rle_lt_trans with (Rdist (sum_f_R0 (fun i:nat => Rabs (An i)) n) (sum_f_R0 (fun i:nat => Rabs (An i)) m)). + assumption. + apply H1; assumption. - destruct (lt_eq_lt_dec n m) as [[ | -> ]|]. + rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ]. unfold Rdist. unfold Rminus. do 2 rewrite Ropp_plus_distr. do 2 rewrite <- Rplus_assoc. do 2 rewrite Rplus_opp_r. do 2 rewrite Rplus_0_l. do 2 rewrite Rabs_Ropp. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n))) . * set (Bn := fun i:nat => An (S n + i)%nat). replace (fun i:nat => Rabs (An (S n + i)%nat)) with (fun i:nat => Rabs (Bn i)). -- apply Rabs_triang_gen. -- unfold Bn; reflexivity. * apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. + unfold Rdist. unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rabs_R0; right; reflexivity. + rewrite (tech2 An m n); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) m n); [ idtac | assumption ]. unfold Rdist. unfold Rminus. do 2 rewrite Rplus_assoc. rewrite (Rplus_comm (sum_f_R0 An m)). rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (An i)) m)). do 2 rewrite Rplus_assoc. do 2 rewrite Rplus_opp_l. do 2 rewrite Rplus_0_r. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m))) . * set (Bn := fun i:nat => An (S m + i)%nat). replace (fun i:nat => Rabs (An (S m + i)%nat)) with (fun i:nat => Rabs (Bn i)). -- apply Rabs_triang_gen. -- unfold Bn; reflexivity. * apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. Qed.
imports: Rbase Rfunctions Rseries Rcomplete