proposition: Lemma Rball_eq_atan_arctan_sum : Rball_eq 0 1 atan arctan_sum.
proof: Proof. intros x x_in ; destruct (Req_dec x 0) as [x_eq | x_neq]. subst ; rewrite atan_0, arctan_sum_0_0 ; reflexivity. pose (lb := Rmin 0 x) ; pose (ub := Rmax 0 x) ; assert (Hbs : lb < ub). apply Rmin_lt_Rmax ; symmetry ; assumption. assert (lb_lb : - 1 < lb). apply Rmin_glb_lt ; [| destruct (Rabs_def2 _ _ x_in)] ; lra. assert (ub_ub : ub < 1). apply Rmax_lub_lt ; [| destruct (Rabs_def2 _ _ x_in)] ; lra. assert (atan_der : forall c, lb < c < ub -> derivable_pt atan c). intros ; apply derivable_atan. assert (arctan_der1 : forall c, lb <= c <= ub -> derivable_pt arctan_sum c). intros ; eapply derivable_Rball_derivable_pt. eapply derivable_Rball_arctan_sum. rewrite Rball_0_simpl ; apply Rabs_def1. apply Rle_lt_trans with ub ; eapply_assumption. apply Rlt_le_trans with lb ; eapply_assumption. assert (arctan_der : forall c, lb < c < ub -> derivable_pt arctan_sum c). intros ; apply arctan_der1 ; split ; left ; eapply_assumption. destruct (MVT arctan_sum atan lb ub) with arctan_der atan_der as [c [c_bd Hc]]. assumption. intros c c_in ; eapply derivable_continuous_pt, arctan_der1 ; assumption. intros ; apply continuity_atan. assert (c_in : Rball 0 1 c). rewrite Rball_0_simpl ; apply Rabs_def1. transitivity ub ; eapply_assumption. transitivity lb ; eapply_assumption. assert (eq_in_0 : atan 0 = arctan_sum 0) by (rewrite atan_0, arctan_sum_0_0 ; reflexivity). assert (eq_in_c : derive_pt arctan_sum c (arctan_der c c_bd) = derive_pt atan c (atan_der c c_bd)). rewrite derive_pt_atan ; apply derive_pt_eq_0, derivable_pt_lim_Rball_pt_lim with 0 1. assumption. apply derivable_pt_lim_Rball_arctan_sum ; assumption. assert (der_neq : derive_pt atan c (atan_der c c_bd) <> 0). rewrite derive_pt_atan ; apply Rinv_neq_0_compat, Rgt_not_eq, One_plus_sqr_pos_lt. unfold ub, lb, Rmin, Rmax in Hc ; destruct (Rle_dec 0 x) as [x_pos | x_neg]. eapply Rminus_eq_compat_rev_strong, eq_in_0. eapply Rmult_eq_compat_r_rev_strong, der_neq ; try eapply eq_in_c. exact Hc. eapply Ropp_eq_compat_rev, Rplus_eq_compat_l_rev_strong, eq_in_0. eapply Rmult_eq_compat_r_rev_strong, der_neq ; try eapply eq_in_c. exact Hc. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5