proposition: Lemma nth_derive_Rball_sum_explicit (k : nat): forall An r x (rAn: finite_cv_radius An r) (rAnk: finite_cv_radius (An_nth_deriv An k) r) (rdAnk: D_Rball 0 r k (sum_r An r rAn)), Rball 0 r x -> nth_derive_Rball 0 r (sum_r An r rAn) rdAnk x = sum_r (An_nth_deriv An k) r rAnk x.
proof: Proof. induction k ; intros An r x rAn rAnk rdAnk x_in. apply sum_r_ext ; symmetry ; apply An_nth_deriv_0. simpl ; assert (rdAn: finite_cv_radius (An_deriv An) r). rewrite <- finite_cv_radius_derivable_compat ; assumption. rewrite nth_derive_Rball_ext with (g := sum_r (An_deriv An) r rdAn) (pr2 := D_Rball_infty_Rpser _ _ rdAn k). assert (rdAnk': finite_cv_radius (An_nth_deriv (An_deriv An) k) r). rewrite <- finite_cv_radius_nth_derivable_compat ; assumption. rewrite sum_r_ext with (rBn := rdAnk'). erewrite (IHk _ _ _ rdAn rdAnk') ; [reflexivity | assumption]. apply An_nth_deriv_S'. intros y y_in ; rewrite derive_Rball_sum_r. apply sum_r_ext ; reflexivity. assumption. assumption. Qed.
imports: Reals Rpow_facts Lra MyRIneq Ranalysis_def Rfunction_def Rextensionality Rsequence_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rinterval Rfunction_classes Nth_derivative_def Nth_derivative_facts