proposition: Lemma TM_atan_correct (x0 : R) (X0 X : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_atan X0 X n) (fun x => Xreal (atan x)).
proof: Proof. move=> Hsubset Hex. apply i_validTM_Ztech with (TR.T_atan tt); last 2 first =>//. exact: I.atan_correct. constructor. - by move=> ? ?; rewrite PolR.size_grec1. - { move=> {X0 n Hsubset Hex} x n k Hx H; rewrite /TR.T_atan /PolR.nth /PolR.grec1 (nth_grec1up_indep _ _ _ _ _ 0%R (m2 := k)) // nth_grec1up_last. case: k H => [|k H]; first by rewrite /= ?Rdiv_1. rewrite last_grec1up // head_gloop1. rewrite [size _]/= subn1 [_.+1.-1]/=. elim: k H x {Hx} =>[|k IHk] H x. + rewrite /= Rmult_0_l Rplus_0_l Rmult_1_r Rdiv_1. symmetry; apply: is_derive_unique; auto_derive =>//. by rewrite Rmult_1_r. + move/ltnW in H; move/(_ H) in IHk. rewrite [INR]lock [PolR.lift]lock [fact]lock /= -!lock. set qk := iteri k (fun i c => PolR.div_mixed_r tt _ (INR (i + 1).+1)) PolR.one in IHk *. rewrite (@Derive_ext _ (fun x => qk.[x] / (1+x*x) ^ (k+1) * INR (fact k.+1))%R); first last. move=> t; move/(_ t) in IHk; rewrite -pow_powerRZ in IHk. rewrite IHk /Rdiv Rmult_assoc Rinv_l ?Rmult_1_r //. exact: INR_fact_neq_0. clear IHk. rewrite PolR.horner_div_mixed_r PolR.horner_sub PolR.horner_add. rewrite PolR.horner_mul_mixed !PolR.horner_lift Derive_scal_l. rewrite Derive_div; first last. * by apply: pow_nonzero; apply: Rsqr_plus1_neq0. * by auto_derive. * exact: PolR.ex_derive_horner. rewrite Derive_pow; try by auto_derive. rewrite Derive_plus; try by auto_derive. rewrite Derive_const ?Rplus_0_l. rewrite Derive_mult; try by auto_derive. rewrite Derive_id. rewrite PolR.Derive_horner. rewrite -{1}(Rmult_1_r (qk^`().[x])) -Rmult_plus_distr_l. rewrite SuccNat2Pos.id_succ. rewrite -addnE addn1 Rmult_1_r Rmult_1_l; simpl predn. rewrite -mul2n (fact_simpl k.+1) 2!mult_INR -[INR 2]/2%R. rewrite -pow_mult multE muln2 -addnn addSnnS pow_add. have ->: (((1 + x * x) ^ k.+1) = (1 + x ^ 2) * (1 + x * x) ^ k)%R by rewrite /= Rmult_1_r. change eq with (@eq R); field. repeat first [ split | exact: INR_fact_neq_0 | exact: not_0_INR | apply pow_nonzero, Rsqr_plus1_neq0 ]. } constructor. - by move=> *; rewrite PolR.size_grec1 Pol.size_grec1. - { move => {X0 X n Hsubset Hex} X0 xi0 n Hx. apply: Pol.grec1_correct =>//. + move=> qi q m Hq. by repeat first [apply: Pol.div_mixed_r_correct| apply: Pol.sub_correct| apply: Pol.add_correct| apply: Pol.deriv_correct| apply: Pol.lift_correct| apply: Pol.mul_mixed_correct| apply: R_from_nat_correct]. + move=> qi q m Hq. by repeat first [apply: J.div_correct| apply: J.power_int_correct| apply: Pol.horner_correct| apply: J.add_correct| apply: J.sqr_correct| apply: I.fromZ_correct| exact: I.fromZ_small_correct| apply: Pol.one_correct]. + exact: Pol.one_correct. + move=> [/=|k]; last by rewrite /PolR.nth !nth_default //; apply: J.zero_correct. exact: J.atan_correct. } - done. - by move=> m x Hx; apply: ex_derive_n_is_derive_n (is_derive_n_atan m x). Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound