proposition: Lemma derivable_pt_lim_in_weaksum_r_strong: forall An r r' (rho : Cv_radius_weak An r) (rho' : Cv_radius_weak (An_deriv An) r') x (x_in: Rball 0 r x) (x_in': Rball 0 r' x), derivable_pt_lim_in (Rball 0 r) (weaksum_r An r rho) x (weaksum_r (An_deriv An) r' rho' x).
proof: Proof. intros An r r' rho rho' x x_in x_in'. assert (r_pos : 0 < r) by (eapply Rball_radius_pos ; eassumption) ; assert (r'_pos : 0 < r') by (eapply Rball_radius_pos ; eassumption) ; assert (min_pos: 0 <= Rmin r r') by (apply MyRIneq.Rmin_pos ; left ; assumption). assert (x_in_min: Rball 0 (Rmin r r') x). unfold Rmin, Rball ; destruct (Rle_dec r r') ; assumption. assert (rho'': Cv_radius_weak An (Rmin r r')). apply Cv_radius_weak_le_compat with r. rewrite Rabs_right ; [rewrite Rabs_right ; [apply Rmin_l | left] | apply Rle_ge ] ; assumption. assumption. assert (rho2: Cv_radius_weak (An_deriv An) (Rmin r r')). apply Cv_radius_weak_le_compat with r'. rewrite Rabs_right ; [rewrite Rabs_right ; [apply Rmin_r | left] | apply Rle_ge ] ; assumption. assumption. assert (Heq: weaksum_r (An_deriv An) r' rho' x = weaksum_r (An_deriv An) (Rmin r r') rho2 x). apply weaksum_r_unique_strong ; [| apply Rmin_glb_lt] ; erewrite <- Rball_0_simpl ; eassumption. rewrite Heq ; eapply derivable_pt_lim_Rball_change ; [eassumption |]. apply derivable_pt_lim_in_ext_strong with (weaksum_r An (Rmin r r') rho''). assumption. intros y y_in ; apply weaksum_r_unique_strong. rewrite <- Rball_0_simpl ; eassumption. rewrite <- Rball_0_simpl ; eapply Rball_included ; [eapply Rmin_l |] ; eassumption. apply derivable_pt_lim_in_weaksum_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