proposition: Lemma derivable_pt_lim_partial_sum : forall (An : nat -> C) (z : C) (n : nat), derivable_pt_lim (fun z => sum_f_C0 (gt_pser An z) n) z (match n with | O => 0 | S _ => sum_f_C0 (gt_pser (An_deriv An) z) (pred n) end).
proof: Proof. intros An z n ; induction n. unfold gt_pser, Cseq_mult ; simpl ; apply derivable_pt_lim_const. destruct n. simpl ; rewrite <- Cadd_0_l ; apply derivable_pt_lim_add ; [apply IHn |]. unfold gt_pser, An_deriv, Cseq_mult, Cseq_shift ; simpl ; rewrite Cmult_1_r, Cmult_1_l. intros eps eps_pos ; exists (mkposreal 1 Rlt_0_1) ; intros ; apply Rle_lt_trans with (Cnorm C0) ; [right ; apply Cnorm_eq_compat ; field | rewrite Cnorm_C0] ; assumption. simpl ; apply derivable_pt_lim_add. apply IHn. apply derivable_pt_lim_gt_pser. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv