proposition: Lemma derivable_pt_lim_sum : forall (An:nat->C) (Pr : infinite_cv_radius An) z, derivable_pt_lim (sum An Pr) z (sum_derive An Pr z).
proof: Proof. intros An Pr z eps eps_pos. assert (H : 0 <= Cnorm z < Cnorm z + 1). split ; [apply Cnorm_pos |] ; intuition. destruct (derivable_pt_lim_weaksum_r _ _ (Pr (Cnorm z + 1)%R) z (proj2 H) _ eps_pos) as [delta Hdelta]. pose (delta' := Rmin delta 1) ; assert (delta'_pos : 0 < delta'). apply Rmin_pos ; [apply delta | apply Rlt_0_1]. exists (mkposreal _ delta'_pos) ; intros h h_neq h_bd. replace (sum An Pr (z + h)) with (weaksum_r An (Cnorm z + 1) (Pr (Cnorm z + 1)%R) (z + h)). apply Hdelta. assumption. apply Rlt_le_trans with delta' ; [assumption | apply Rmin_l]. unfold sum. apply weaksum_r_unique_strong. apply Rle_lt_trans with (Cnorm z + Cnorm h)%R. apply Cnorm_triang. apply Rplus_lt_compat_l ; apply Rlt_le_trans with delta' ; [intuition | apply Rmin_r]. intuition. 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