proposition: Lemma derivable_pt_lim_weaksum_r : forall (An:nat->C) (r:R) (Pr : Cv_radius_weak An r) z, Cnorm z < r -> derivable_pt_lim (weaksum_r An r Pr) z (weaksum_r_derive An r Pr z).
proof: Proof. intros An r rho z z_bd. assert (r_pos : 0 < r) by (apply Rle_lt_trans with (Cnorm z) ; [apply Cnorm_pos | assumption]). pose (midd := middle (Cnorm z) r) ; assert (midd_pos : 0 < midd). unfold midd ; apply middle_le_lt_pos_lt ; [apply Cnorm_pos | assumption]. pose (r' := mkposreal midd midd_pos). assert (z_bd' : Cnorm z < midd). apply (middle_is_in_the_middle _ _ z_bd). assert (r'_ub : r' < r). apply (proj2 (middle_is_in_the_middle _ _ z_bd)). pose (fn := fun N z => sum_f_C0 (gt_pser An z) N) ; pose (fn' := fun N z => Cpser_partial_sum_derive An N z) ; pose (f := weaksum_r An r rho) ; pose (g := weaksum_r_derive An r rho). assert (z_in : Boule 0 r' z). unfold Boule ; simpl ; unfold C_dist ; rewrite Cnorm_minus_sym, Cminus_0_r ; assumption. assert (fn_deriv : forall (x : C) (n : nat), Boule 0 r' x -> derivable_pt_lim (fn n) x (fn' n x)). intros ; apply Cpser_derive_finite_sum. assert (fn_cv : CFseq_cv_boule fn f 0 r'). intros a a_in. assert (a_bd : Cnorm a < r). unfold Boule in a_in ; simpl in a_in ; unfold C_dist in a_in ; rewrite Cnorm_minus_sym, Cminus_0_r in a_in. apply Rlt_trans with midd ; assumption. assert (H := weaksum_r_sums An r rho a a_bd). intros eps eps_pos ; destruct (H eps eps_pos) as [N HN] ; exists N ; intros n n_lb ; unfold fn, f ; simpl in HN ; unfold C_dist in HN. apply HN ; assumption. assert (cv : forall z : C, Boule 0 r' z -> {l : C | Cseq_cv (fun N : nat => CFpartial_sum (fun n : nat => (fun (n0 : nat) (z0 : C) => gt_pser (An_deriv An) z0 n0) n z) N) l}). intros a a_in. exists (weaksum_r_derive An r rho a). apply Pser_Cseqcv_link ; apply weaksum_r_derive_sums. apply Rlt_trans with r' ; [unfold Boule in a_in ; simpl in a_in ; unfold C_dist in a_in ; rewrite Cminus_0_l, Cnorm_opp in a_in ; apply a_in | assumption]. assert (r''_comp : Rabs (middle r' r) < Rabs r). rewrite Rabs_right ; [rewrite Rabs_right |]. apply (proj2 (middle_is_in_the_middle _ _ r'_ub)). left ; assumption. left ; apply middle_le_lt_pos_lt. left ; unfold r' ; apply middle_le_lt_pos_lt ; [apply Cnorm_pos | assumption]. assumption. assert (rho_An' := Cv_radius_weak_derivable_compat An r rho (middle r' r) r''_comp). assert (cvn_r : CVN_r (fun (n : nat) (z : C) => gt_pser (An_deriv An) z n) r'). apply Cpser_abel2 with (middle r' r). assumption. apply (proj1 (middle_is_in_the_middle _ _ r'_ub)). assert (fn'_cvu := CVN_CVU_boule (fun n z => gt_pser (An_deriv An) z n) r' cv cvn_r). assert (fn'_cvu2 : CFseq_cvu fn' g 0 r'). unfold fn', g. intros eps eps_pos ; destruct (fn'_cvu _ eps_pos) as [N HN] ; exists (S N) ; clear fn'_cvu fn_deriv rho_An' ; intros n y n_lb y_bd. assert (H : n = S (pred n)) by intuition ; rewrite H ; clear H ; simpl. unfold CFseq_cvu, SFL_interv, CFpartial_sum in HN. assert (predn_lb : (N <= pred n)%nat) by intuition. assert (Temp := HN (pred n) y predn_lb y_bd). destruct (Rlt_le_dec (Cnorm (0 - y)) r') as [H | Hf]. destruct (cv y H) as [l Hl]. assert (Hrew : l = weaksum_r_derive An r rho y). eapply Cseq_cv_unique ; [apply Hl |] ; apply Pser_Cseqcv_link ; apply weaksum_r_derive_sums. apply Rlt_trans with r' ; [rewrite Cminus_0_l, Cnorm_opp in H |] ; assumption. rewrite <- Hrew ; assumption. clear - y_bd Hf ; assert (Hf2 : Cnorm (0 - y) < Cnorm (0 - y)) by (apply Rlt_le_trans with r' ; assumption) ; elim (Rlt_irrefl _ Hf2). assert (g_cont : (forall x : C, Boule 0 r' x -> continuity_pt g x)). intros a a_in ; apply CVU_continuity_boule with fn' C0 r'. apply fn'_cvu2. intros N y y_in ; unfold fn'. unfold Cpser_partial_sum_derive ; induction N. apply continuity_pt_const ; unfold constant ; intros ; trivial. destruct N ; simpl ; [unfold gt_pser, An_deriv |]. intros eps eps_pos ; exists R1 ; split ; [apply Rlt_0_1 |] ; intros x [_ Hx] ; simpl ; unfold C_dist ; repeat rewrite Cpow_0. unfold Cminus ; rewrite Cadd_opp_r, Cnorm_C0 ; assumption. apply continuity_pt_add ; [assumption |]. unfold gt_pser. apply continuity_pt_mult. apply continuity_pt_const. intros r1 r2 ; unfold An_deriv ; reflexivity. apply derivable_continuous ; apply derivable_Cpow. assumption. exact (CFseq_cvu_derivable fn fn' f g z 0 r' z_in fn_deriv fn_cv fn'_cvu2 g_cont). Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts