proposition: Lemma weaksum_r_derive_sums : forall (An : nat -> C) (r : R) (Pr : Cv_radius_weak An r) (z : C), Cnorm z < r -> Cpser (An_deriv An) z (weaksum_r_derive An r Pr z).
proof: Proof. intros An r Pr z z_bd. unfold weaksum_r_derive ; case (Rlt_le_dec (Cnorm z) r) ; intro s. rewrite <- Rabs_right in z_bd. apply weaksum_r_sums ; apply (proj1 (middle_is_in_the_middle _ _ z_bd)). apply Rle_ge ; apply Rle_trans with (Cnorm z) ; [apply Cnorm_pos | left ; assumption]. assert (H : Cnorm z < Cnorm z) by (apply Rlt_le_trans with r ; assumption) ; elim (Rlt_irrefl _ H). 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