proposition: Lemma derive_Rball_weaksum_r: forall An r (rho : Cv_radius_weak An r) pr, (derive_Rball 0 r (weaksum_r An r rho) pr == weaksum_r_derive An r rho)%F.
proof: Proof. intros An r rho pr x ; unfold derive_Rball, weaksum_r_derive. destruct (Rlt_le_dec (Rabs x) r) as [x_bd | x_nbd] ; destruct (in_Rball_dec 0 r x) as [x_in | x_nin]. destruct (pr x x_in) as [l Hl] ; simpl. assert (r_pos : 0 <= r) by (left ; eapply Rball_radius_pos ; eassumption) ; eapply derivable_pt_lim_Rball_uniqueness ; try eassumption. assert (mid_pos: 0 <= middle (Rabs x) r) by (apply middle_le_le_pos ; [apply Rabs_pos | assumption]). apply derivable_pt_lim_in_weaksum_r_strong. assumption. apply Rball_0_simpl, middle_is_in_the_middle ; assumption. exfalso ; apply x_nin, Rball_0_simpl ; assumption. exfalso ; apply (Rlt_irrefl (Rabs x)) ; apply Rlt_le_trans with r. erewrite <- Rball_0_simpl ; eassumption. assumption. reflexivity. 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