proposition: Lemma derivable_pt_in_weaksum_r: forall An r (rho : Cv_radius_weak An r) x (x_in: Rball 0 r x), derivable_pt_in (Rball 0 r) (weaksum_r An r rho) x.
proof: Proof. intros An r rho x x_in ; assert (r_pos : 0 <= r) by (left ; eapply Rball_radius_pos ; eassumption) ; pose (r' := middle (Rabs x) r) ; assert (r'_pos: 0 <= r'). apply middle_le_le_pos ; [apply Rabs_pos | assumption]. assert (rho': Cv_radius_weak (An_deriv An) r'). eapply Cv_radius_weak_derivable_compat ; [eassumption|]. rewrite Rabs_right ; [rewrite (Rabs_right r) |]. apply middle_is_in_the_middle ; erewrite <- Rball_0_simpl ; eassumption. apply Rle_ge ; assumption. apply Rle_ge ; assumption. exists (weaksum_r (An_deriv An) r' rho' x). apply derivable_pt_lim_in_weaksum_r_strong. assumption. apply Rball_0_simpl, middle_is_in_the_middle ; erewrite <- Rball_0_simpl ; eassumption. 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