proposition: Lemma derivable_pt_lim_weaksum_r : forall An r (Pr : Cv_radius_weak An r) x, Rabs x < r -> derivable_pt_lim (weaksum_r An r Pr) x (weaksum_r_derive An r Pr x).
proof: Proof. intros An r rho x x_in ; unfold weaksum_r_derive ; assert (r_pos: 0 <= r) by (left ; apply Rle_lt_trans with (Rabs x) ; [apply Rabs_pos | assumption]) ; destruct (Rlt_le_dec (Rabs x) r) as [x_bd | x_nbd]. apply derivable_pt_lim_Rball_pt_lim with 0 r. apply Rball_0_simpl ; assumption. assert (r'_pos: 0 <= middle (Rabs x) r) by (apply middle_le_le_pos ; [apply Rabs_pos | assumption]). apply derivable_pt_lim_in_weaksum_r_strong ; rewrite Rball_0_simpl ; [| eapply middle_is_in_the_middle] ; assumption. exfalso ; apply Rlt_irrefl with (Rabs x), Rlt_le_trans with r ; 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