proposition: Lemma atan_eq_ps_atan : forall x, 0 < x < 1 -> atan x = ps_atan x.
proof: Proof. intros x x_encad. assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c). { intros c c_encad. apply derivable_pt_minus. { exact (derivable_pt_atan c). } apply derivable_pt_ps_atan. destruct x_encad; destruct c_encad; split; lra. } assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c). { intros ; apply derivable_pt_id; lra. } assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c). { intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]]; apply continuity_pt_minus. - apply derivable_continuous_pt ; apply derivable_pt_atan. - apply derivable_continuous_pt ; apply derivable_pt_ps_atan. split; destruct x_encad; lra. - apply derivable_continuous_pt, derivable_pt_atan. - apply derivable_continuous_pt, derivable_pt_ps_atan. subst c; destruct x_encad; split; lra. - apply derivable_continuous_pt, derivable_pt_atan. - apply derivable_continuous_pt, derivable_pt_ps_atan. subst c; split; lra. - apply derivable_continuous_pt, derivable_pt_atan. - apply derivable_continuous_pt, derivable_pt_ps_atan. subst c; destruct x_encad; split; lra. } assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c). { intros ; apply derivable_continuous ; apply derivable_id. } assert (x_lb : 0 < x) by (destruct x_encad; lra). elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main. clear - Main x_encad. assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0). { intro pr. assert (d_encad3 : -1 < d < 1). { destruct d_encad; destruct x_encad; split; lra. } pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)). rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr). - unfold pr3. rewrite derive_pt_minus. rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d). { intuition. } assumption. - destruct d_encad; lra. - assumption. - reflexivity. } assert (iatan0 : atan 0 = 0). { apply tan_inj. - apply atan_bound. - rewrite Rdiv_opp_l; assert (t := PI2_RGT_0); split; lra. - rewrite tan_0, tan_atan; reflexivity. } generalize Main; rewrite Temp, Rmult_0_r. replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition. replace ((atan - ps_atan)%F 0) with (atan 0 - ps_atan 0) by intuition. rewrite iatan0, ps_atan0_0, !Rminus_0_r. replace (derive_pt id d (pr2 d d_encad)) with 1. { rewrite Rmult_1_r. solve[intros M; apply Rminus_diag_uniq; auto]. } rewrite pr_nu_var with (g:=id) (pr2:=derivable_pt_id d). { symmetry ; apply derive_pt_id. } tauto. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia