proposition: Lemma CVN_R_CVS : forall fn:nat -> R -> R, CVN_R fn -> forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }.
proof: Proof. intros; apply R_complete. unfold SP; set (An := fun N:nat => fn N x). change (Cauchy_crit_series An). apply cauchy_abs. unfold Cauchy_crit_series; apply CV_Cauchy. pose proof (Rabs_pos x) as Rabs_pos_x. unfold CVN_R in X; cut (0 < Rabs x + 1). 2:{ lra. } intro; assert (H0 := X (mkposreal _ H)). unfold CVN_r in H0; elim H0; intros Bn H1. elim H1; intros l H2. elim H2; intros. apply Rseries_CV_comp with Bn. { intro; split. { apply Rabs_pos. } unfold An; apply H4; unfold Boule; simpl; rewrite Rminus_0_r. lra. } exists l. assert (forall n:nat, 0 <= Bn n). { intro; apply Rle_trans with (Rabs (An n)). { apply Rabs_pos. } unfold An; apply H4; unfold Boule; simpl; rewrite Rminus_0_r; lra. } unfold Un_cv in H3; unfold Un_cv; intros. elim (H3 _ H6); intros. exists x0; intros. replace (sum_f_R0 Bn n) with (sum_f_R0 (fun k:nat => Rabs (Bn k)) n). - apply H7; assumption. - apply sum_eq; intros; apply Rabs_right; apply Rle_ge; apply H5. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra