proposition: Lemma derive_pt_atan : forall x, derive_pt atan x (derivable_pt_atan x) = 1 / (1 + x²).
proof: Proof. intros x. destruct (frame_tan x) as [ub [[ub0 ubpi] Pub]]. assert (lb_lt_ub : -ub < ub) by apply pos_opp_lt, ub0. assert (xint : tan(-ub) < x < tan ub). { assert (xint' : x < tan ub /\ -(tan ub) < x) by apply Rabs_def2, Pub. rewrite tan_neg; tauto. } assert (inv_p : forall x, tan(-ub) <= x -> x <= tan ub -> comp tan atan x = id x). { intros; apply tan_atan. } assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> -ub <= atan y <= ub). { clear -ub0 ubpi; intros y lo up; split. { destruct (Rle_lt_dec (-ub) (atan y)) as [h | abs]; auto. assert (y < tan (-ub)). { rewrite <- (tan_atan y); apply tan_increasing. - destruct (atan_bound y); assumption. - assumption. - lra. } lra. } destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). { rewrite <- (tan_atan y); apply tan_increasing. - rewrite Rdiv_opp_l; lra. - assumption. - destruct (atan_bound y); assumption. } lra. } assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). { intros y z l yz u; apply tan_increasing. - rewrite Rdiv_opp_l; lra. - assumption. - lra. } assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). { intros a [la ua]; apply derivable_pt_tan. rewrite Rdiv_opp_l; split; lra. } assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint int_tan der) <> 0). { rewrite <- (pr_nu tan (atan x) (derivable_pt_tan (atan x) (atan_bound x))). rewrite derive_pt_tan. solve[apply Rgt_not_eq, plus_Rsqr_gt_0]. } assert (t := derive_pt_recip_interv tan atan (-ub) ub x lb_lt_ub xint incr int_tan der inv_p df_neq). rewrite <- (pr_nu atan x (derivable_pt_recip_interv tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der df_neq)). rewrite t. assert (t' := atan_bound x). rewrite <- (pr_nu tan (atan x) (derivable_pt_tan _ t')). rewrite derive_pt_tan, tan_atan. replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia