proposition: Lemma derivable_pt_lim_ps_atan : forall x, -1 < x < 1 -> derivable_pt_lim ps_atan x ((fun y => /(1 + y ^ 2)) x).
proof: Proof. intros x x_encad. destruct (boule_in_interval (-1) 1 x x_encad) as [c [r [Pcr1 [P1 P2]]]]. change (/ (1 + x ^ 2)) with ((fun u => /(1 + u ^ 2)) x). assert (t := derivable_pt_lim_CVU). apply derivable_pt_lim_CVU with (fn := (fun N x => sum_f_R0 (tg_alt (Ratan_seq x)) N)) (fn' := (fun N x => sum_f_R0 (tg_alt (Datan_seq x)) N)) (c := c) (r := r). - assumption. - intros y N inb; apply Rabs_def2 in inb; destruct inb. apply Datan_is_datan. { lra. } lra. - intros y inb; apply Rabs_def2 in inb; destruct inb. assert (y_gt_0 : -1 < y) by lra. assert (y_lt_1 : y < 1) by lra. intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos). intros N HN ; exists N; intros n n_lb ; apply HN ; tauto. - apply Datan_CVU_prelim. replace ((c - r + (c + r)) / 2) with c by field. unfold mkposreal_lb_ub; simpl. replace ((c + r - (c - r)) / 2) with (r :R) by field. assert (Rabs c < 1 - r). { unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1; apply Rabs_def2 in Pcr1; destruct Pcr1; lra. } lra. - intros; apply Datan_continuity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia