proposition: Lemma D_Rball_infty_Rpser: forall An r (rho: finite_cv_radius An r), D_Rball_infty 0 r (sum_r An r rho).
proof: Proof. intros An r rho n ; revert rho ; revert r ; revert An ; induction n ; intros An r rho. constructor. apply Db_S with (derivable_Rball_sum_r An r rho). apply D_Rball_ext with (sum_r_derive An r rho). intros x x_in ; symmetry ; apply derivable_pt_lim_in_derive_Rball. assumption. apply derivable_pt_lim_in_sum_r ; assumption. apply IHn. Qed.
imports: Reals Rsequence_def Rfunction_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def Rfunction_classes_facts Rextensionality Rpser_def Rpser_def Rpser_cv_facts Rpser_sums Rpser_sums_facts Rpser_derivative