proposition: Lemma derivable_pt_lim_sum_r : forall An r (Pr : finite_cv_radius An r) z, Rabs z < r -> derivable_pt_lim (sum_r An r Pr) z (sum_r_derive An r Pr z).
proof: Proof. intros An r rho z z_bd eps eps_pos. assert (z_bd2 : Rabs z < middle (Rabs z) r) by (apply middle_is_in_the_middle ; assumption). assert (pr : Cv_radius_weak An (middle (Rabs z) r)). apply (proj1 rho) ; split ; [left ; apply middle_le_lt_pos_lt | apply middle_is_in_the_middle] ; [| apply Rle_lt_trans with (Rabs z) |] ; (apply Rabs_pos || assumption). destruct (derivable_pt_lim_weaksum_r _ _ pr z z_bd2 eps eps_pos) as [d1 Hd1]. pose (d2 := middle (Rabs z) r - Rabs z). assert (d2_pos : 0 < d2). unfold d2 ; apply Rlt_Rminus ; apply middle_is_in_the_middle ; assumption. pose (d := Rmin d1 d2). assert (d_pos : 0 < d). unfold d ; apply Rmin_pos_lt ; [apply d1 | assumption]. pose (delta := mkposreal d d_pos) ; exists delta ; intros h h_neq h_bd. assert (Rabs (z + h) < middle (Rabs z) r). apply Rle_lt_trans with (Rabs z + Rabs h) ; [apply Rabs_triang |]. apply Rlt_le_trans with (Rabs z + delta). apply Rplus_lt_compat_l ; assumption. apply Rle_trans with (Rabs z + (middle (Rabs z) r - Rabs z)). apply Rplus_le_compat_l ; unfold delta ; apply Rmin_r. right ; ring. assert (Rabs (z + h) < r). apply Rlt_trans with (middle (Rabs z) r) ; [| apply middle_is_in_the_middle] ; assumption. specialize (Hd1 h h_neq). repeat erewrite sum_r_unfold. eapply Rle_lt_trans ; [| eapply Hd1]. right ; apply Rabs_eq_compat ; apply Rminus_eq_compat. reflexivity. unfold weaksum_r_derive, sum_r_derive ; destruct (Rlt_le_dec (Rabs z) (middle (Rabs z) r)) as [z_bd' | Hf]. apply sum_r_unfold ; [| do 2 apply middle_is_in_the_middle] ; assumption. assert (T := proj1 (middle_is_in_the_middle _ _ z_bd)) ; clear - Hf T ; exfalso ; lra. apply Rlt_le_trans with delta ; [assumption | unfold delta ; apply Rmin_l]. assumption. assumption. assumption. assumption. 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