proposition: Lemma CVN_CVU_boule :forall (fn : nat -> C -> C) (r : posreal) (cv : forall z : C, Boule 0 r z -> {l : C | Cseq_cv (fun N : nat => CFpartial_sum (fun n => fn n z) N) l}), CVN_r fn r -> CFseq_cvu (fun N z => CFpartial_sum (fun n => fn n z) N) (SFL_interv fn r cv) 0 r.
proof: Proof. intros fn r cv cvn eps eps_pos. destruct cvn as [An [l [sum_cv fn_bd]]] ; destruct (sum_cv eps eps_pos) as [N HN] ; exists N ; intros n y n_lb y_bd. unfold SFL_interv. destruct (Rlt_le_dec (Cnorm (0 - y)) r) as [y_bd2 | y_lb]. destruct (cv y y_bd2) as [l2 Hl2] ; unfold C_dist. apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k => Cnorm (An k)) n - l)). rewrite <- (Rabs_Ropp (sum_f_R0 (fun k:nat => Cnorm (An k)) n - l)); rewrite Ropp_minus_distr'; rewrite (Rabs_right (l - sum_f_R0 (fun k:nat => Cnorm (An k)) n)). rewrite Cnorm_minus_sym ; eapply sum_maj1. apply Hl2. apply sum_cv. intros ; apply fn_bd ; assumption. apply Rge_minus ; apply Rle_ge ; apply sum_incr. assumption. intros ; apply Cnorm_pos. unfold R_dist in HN ; apply HN ; assumption. unfold Boule in y_bd ; simpl in y_bd ; unfold C_dist in y_bd. assert (Hf : Cnorm (0 - y) < Cnorm (0 - y)). apply Rlt_le_trans with r ; assumption. destruct (Rlt_irrefl _ Hf). Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv