proposition: Lemma CVN_CVU_interv : forall (fn:nat -> R -> R) (r:posreal) (cv:forall x:R, Boule 0 r x -> {l:R | Un_cv (fun N:nat => SP fn N x) l }), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL_interv fn r cv) 0 r.
proof: Proof. intros; unfold CVU in |- *; intros. unfold CVN_r in X. elim X; intros An X0. elim X0; intros s H0. elim H0; intros. cut (Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n - s) 0). intro; 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)). 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 in |- *; case (cv y H6) ; intro. unfold SFL_interv. case (Rlt_le_dec y r) ; intro y_bd1. case (Rlt_le_dec (- r) y) ; intro y_bd2. destruct (cv y (Rabs_def1 (y - 0) r (eq_ind_r (fun r0 : R => r0 < r) y_bd1 (Rminus_0_r y)) (eq_ind_r (fun r0 : R => - r < r0) y_bd2 (Rminus_0_r y)))) as (l, Hl). trivial. clear -H6 y_bd1 y_bd2 ; destruct (Rabs_def2 _ _ H6) as [H1 H2] ; rewrite Rminus_0_r in H1, H2 ; apply False_ind ; apply Rlt_irrefl with (-r) ; apply Rlt_le_trans with y ; assumption. clear -H6 y_bd1; destruct (Rabs_def2 _ _ H6) as [H1 H2] ; rewrite Rminus_0_r in H1, H2 ; apply False_ind ; apply Rlt_irrefl with y ; apply Rlt_le_trans with r ; assumption. 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 in |- *; rewrite (Rplus_comm s); rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; apply sum_incr. apply H1. intro; apply Rabs_pos. unfold R_dist in H4; unfold Rminus in H4; rewrite Ropp_0 in H4. assert (H7 := H4 n H5). rewrite Rplus_0_r in H7; apply H7. unfold Un_cv in H1; unfold Un_cv in |- *; intros. elim (H1 _ H3); intros. exists x; intros. unfold R_dist in |- *; unfold R_dist in H4. rewrite Rminus_0_r; apply H4; assumption. Qed.
imports: Reals RFsequence Lra PeanoNat