proposition: Lemma derivable_pt_lim_sum : forall An (Pr : infinite_cv_radius An), forall z, derivable_pt_lim (sum An Pr) z (sum_derive An Pr z).
proof: Proof. intros An rho z eps eps_pos. assert (z_bd : Rabs z < Rabs z + 1) by lra. destruct (derivable_pt_lim_weaksum_r _ _ (rho _) _ z_bd _ eps_pos) as [d Hd]. pose (d' := Rmin d (1 / 2)). assert (d'_pos : 0 < d'). unfold Rmin ; apply Rmin_pos_lt ; [apply d | lra]. pose (delta := mkposreal d' d'_pos) ; exists delta ; intros h h_neq h_bd ; specialize (Hd h h_neq); eapply Rle_lt_trans ; [| eapply Hd]. right ; apply Rabs_eq_compat ; apply Rminus_eq_compat. unfold Rdiv ; apply Rmult_eq_compat_r ; unfold sum ; apply Rminus_eq_compat ; apply weaksum_r_unique_strong ; auto. apply Rle_lt_trans with (Rabs (z + h) + 0) ; [right ; ring | lra]. apply Rle_lt_trans with (Rabs z + Rabs h) ; [apply Rabs_triang |] ; apply Rplus_lt_compat_l ; apply Rlt_trans with (1/2) ; [apply Rlt_le_trans with delta |] ; [| unfold delta ; apply Rmin_r |] ; lra. unfold sum_derive, sum, weaksum_r_derive ; destruct (Rlt_le_dec (Rabs z) (Rabs z + 1)) as [H | Hf]. apply weaksum_r_unique_strong ; [| apply middle_is_in_the_middle] ; assumption. exfalso ; apply (Rlt_irrefl (Rabs z)) ; apply Rlt_le_trans with (Rabs z + 1) ; lra. apply Rlt_le_trans with delta ; [assumption | unfold delta ; apply Rmin_l]. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics