proposition: Lemma CVN_CVU : forall (fn:nat -> R -> R) (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l }) (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
proof: Proof. intros; unfold CVU; intros. unfold CVN_r in X. elim X; intros An X0. elim X0; intros s H0. elim H0; intros. assert (Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n - s) 0). { unfold Un_cv in H1; unfold Un_cv; intros. elim (H1 _ H3); intros. exists x; intros. unfold Rdist; unfold Rdist in H4. rewrite Rminus_0_r; apply H4; assumption. } unfold Un_cv in H3. elim (H3 eps H); intros N0 H4. exists N0; intros. apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => Rabs (An k)) n - s)). 2:{ unfold Rdist in H4; unfold Rminus in H4; rewrite Ropp_0 in H4. assert (H7 := H4 n H5). rewrite Rplus_0_r in H7; apply H7. } rewrite <- (Rabs_Ropp (sum_f_R0 (fun k:nat => Rabs (An k)) n - s)); rewrite Ropp_minus_distr; rewrite (Rabs_right (s - sum_f_R0 (fun k:nat => Rabs (An k)) n)). { eapply sum_maj1. - unfold SFL; case (cv y); intro. trivial. - apply H1. - intro; elim H0; intros. rewrite (Rabs_right (An n0)). + apply H8; apply H6. + apply Rle_ge; apply Rle_trans with (Rabs (fn n0 y)). * apply Rabs_pos. * apply H8; apply H6. } apply Rle_ge; apply Rplus_le_reg_l with (sum_f_R0 (fun k:nat => Rabs (An k)) n). rewrite Rplus_0_r; unfold Rminus; rewrite (Rplus_comm s); rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; apply sum_incr. - apply H1. - intro; apply Rabs_pos. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra