proposition: Lemma derivable_pt_lim_Rball_arctan_sum : forall x, Rball 0 1 x -> derivable_pt_lim_in (Rball 0 1) arctan_sum x (/ (1 + x ^ 2)).
proof: Proof. intros x x_in. assert (x_bd : Rabs x < 1) by (rewrite <- Rball_0_simpl ; assumption). assert (x2_bd : Rabs (x ^ 2) < 1). rewrite <- RPow_abs ; apply Rpow_lt_1_compat ; [apply Rabs_pos | assumption]. eapply derivable_pt_lim_in_ext_strong. assumption. intros y y_in ; eapply Rpser_unique, arctan_sum_sums. apply sum_r_sums with (Pr := arctan_cv_radius). rewrite <- Rball_0_simpl ; assumption. split ; [| left] ; destruct (Rabs_def2 _ _ y_in) ; lra. replace (/ (1 + x ^ 2)) with (sum_r_derive arctan_seq 1 arctan_cv_radius x). apply derivable_pt_lim_in_sum_r ; assumption. transitivity (sum_pow (- x ^ 2)). assert (rho1 : finite_cv_radius (Rseq_alt sum_pow_seq) 1). rewrite <- finite_cv_radius_alt_compat ; apply sum_pow_cv_radius. assert (rho2 : finite_cv_radius (Rseq_zip (Rseq_alt sum_pow_seq) 0) 1). rewrite <- Rsqrt_sqr with (y := nnr_sqr 1) ; [| lra | simpl ; ring] ; apply finite_cv_radius_zip_compat_l. simpl nonneg ; repeat rewrite Rmult_1_l ; apply rho1. intros ; apply zero_infinite_cv_radius. unfold sum_r_derive ; rewrite sum_r_ext with (rBn := rho2) ; [| eapply An_deriv_arctan_seq_explicit]. rewrite sum_r_zip_compat_0_l with (rAn := rho1) ; try assumption. apply sum_r_alt_compat ; assumption. transitivity (/ (1 - (- x ^ 2))). apply sum_pow_explicit ; rewrite Rabs_Ropp ; assumption. unfold Rminus ; rewrite Ropp_involutive ; reflexivity. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rpser_sums_facts