proposition: Lemma TM_power_int_correct_aux (p : Z) (x0 : R) (X0 X : I.type) n : (0 <= p)%Z \/ apart0 X -> subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (let P := (T_power_int prec p X0 n) in RPA P (Ztech (T_power_int prec p) P (fun x => I.power_int prec x p) X0 X n)) (fun x => Xpower_int' x p).
proof: Proof. move=> Hyp Hsubset Hex. apply i_validTM_Ztech with (TR.T_power_int tt p); last 2 first =>//. exact: I.power_int_correct. constructor. - by move=> {n} ? n; rewrite ?(@PolR.size_dotmuldiv n.+1, @Pol.size_dotmuldiv n.+1, Pol.size_rec1, size_rec1up, PolR.size_rec1) //. - { move=> x m k Hx Hk. rewrite /TR.T_power_int PolR.nth_dotmuldiv ifF; last first. rewrite PolR.size_rec1. rewrite size_falling_seq size_fact_seq. by rewrite !orbb ltnNge Hk. case: k Hk => [|k] Hk. simpl Derive_n; simpl INR; rewrite Rdiv_1. rewrite falling_seq_correct // fact_seq_correct //. rewrite big_mkord big_ord0. rewrite [PolR.nth _ _]nth_rec1up /= Rdiv_1 Rmult_1_l. rewrite toR_power_int //. by case: Hyp => [Hyp|Hyp]; by [left|right; exact: apart0_correct Hyp]. rewrite -(Derive_n_ext_loc _ _ k.+1 x (toR_power_int_loc _)); last by case: Hyp => [Hyp|Hyp]; by [left|right; exact: apart0_correct Hyp]. symmetry; apply: (Rmult_eq_reg_r (INR (fact k.+1))); last exact: INR_fact_neq_0. rewrite {1}/Rdiv Rmult_assoc Rinv_l ?Rmult_1_r; last exact: INR_fact_neq_0. clear - Hyp Hk Hx. rewrite /powerRZ. case: p Hyp Hx =>[|p|p] Hyp Hx. - rewrite Derive_n_const. rewrite /PolR.nth /PolR.rec1 nth_rec1up ifF; last first. by apply: negbTE; rewrite ltnNge Hk. rewrite iteriS /TR.pow_aux_rec ifF ?(Rmult_0_r, Rmult_0_l) //. apply: negbTE; rewrite negb_or /=; apply/negP; move/Z.geb_le. by change Z0 with (Z.of_nat O); move/Nat2Z.inj_le/leP; rewrite addn1. - rewrite (is_derive_n_unique _ _ _ _ (is_derive_n_pow _ _ _ _)); last first. exact/ltP/Pos2Nat.is_pos. rewrite falling_seq_correct // fact_seq_correct //. have Hpow: PolR.nth (PolR.rec1 (TR.pow_aux_rec tt (Z.pos p) x) (x ^ Pos.to_nat p) m)%R k.+1 = if (Z.of_nat (k + 1) <=? Z.pos p)%Z then (x ^ (Pos.to_nat p - k.+1))%R else 0%R. rewrite /PolR.nth /PolR.rec1 nth_rec1up. rewrite ifF; last first. by apply: negbTE; rewrite ltnNge Hk. case: Z.leb_spec. move=> /Zle_is_le_bool Hpk; rewrite iteriS /TR.pow_aux_rec Z.geb_leb Hpk. rewrite orbT pow_powerRZ; congr powerRZ. rewrite Nat2Z.inj_sub ?(positive_nat_Z, addn1) //. apply/Nat2Z.inj_le; rewrite positive_nat_Z -addn1. by move: Hpk; case: Z.leb_spec. move=> Hpk; rewrite iteriS /TR.pow_aux_rec Z.geb_leb ifF //. apply: negbTE; rewrite negb_or /=. by rewrite -Z.ltb_antisym; move/Zlt_is_lt_bool in Hpk. case: (Z.leb_spec (Z.of_nat (k + 1)) (Z.pos p)) => Hpk. move/Zle_is_le_bool in Hpk. rewrite Hpow Hpk. rewrite /Rdiv; ring_simplify . rewrite -INR_IZR_INZ Rmult_assoc Rinv_l; last exact: INR_fact_neq_0. rewrite Rmult_1_r Rmult_comm; congr Rmult. rewrite (big_morph IZR (id1 := 1%R) (op1 := Rmult)) //; last exact: mult_IZR. rewrite big_mkord; apply: eq_bigr => [[i Hi] _]. rewrite INR_IZR_INZ. rewrite Nat2Z.inj_sub ?(positive_nat_Z, addn1) //=. apply/leP; rewrite ltnS in Hi. apply: leq_trans Hi _. move/Zle_is_le_bool in Hpk. rewrite -positive_nat_Z in Hpk; move/Nat2Z.inj_le/leP in Hpk. by apply: leq_trans _ Hpk; rewrite addn1. rewrite [in LHS]big_ord_recr big_mkord [in RHS]big_ord_recr. try simpl (Rmul_monoid _ _). have->: Pos.to_nat p - k = 0. rewrite -positive_nat_Z addn1 in Hpk; move/Nat2Z.inj_lt/ltP in Hpk. rewrite ltnS in Hpk. by apply/eqP; rewrite subn_eq0. rewrite Hpow ifF /= ?Rmult_0_l ?Rmult_0_r ?Rmult_0_l//. apply: negbTE. by move/Zlt_is_lt_bool: Hpk; rewrite Z.ltb_antisym =>->. - rewrite (is_derive_n_unique _ _ _ _ (is_derive_n_inv_pow _ _ _ _ _)); first last. case: Hyp; first case =>//. by move/apart0_correct; apply. exact/ltP/Pos2Nat.is_pos. rewrite falling_seq_correct // fact_seq_correct //. have Hpow: PolR.nth (PolR.rec1 (TR.pow_aux_rec tt (Z.neg p) x) (/ x ^ Pos.to_nat p) m)%R k.+1 = (/ x ^ (Pos.to_nat p + k.+1))%R. rewrite /PolR.nth /PolR.rec1 nth_rec1up. rewrite ifF; last first. by apply: negbTE; rewrite ltnNge Hk. rewrite iteriS /TR.pow_aux_rec addn1 /= Pos.of_nat_succ. by rewrite Pos2Nat.inj_add Nat2Pos.id. rewrite Hpow. rewrite /Rdiv; ring_simplify . rewrite -INR_IZR_INZ Rmult_assoc Rinv_l; last exact: INR_fact_neq_0. rewrite Rmult_1_r Rmult_comm; congr Rmult. rewrite (big_morph IZR (id1 := 1%R) (op1 := Rmult)) //; last exact: mult_IZR. rewrite big_mkord; apply: eq_bigr => [[i Hi] _]. rewrite INR_IZR_INZ -opp_IZR; congr IZR. rewrite Nat2Z.inj_add positive_nat_Z. by rewrite Z.opp_add_distr. } constructor. - by move=> {n} ? ? n; rewrite ?(@PolR.size_dotmuldiv n.+1, @Pol.size_dotmuldiv n.+1, Pol.size_rec1, size_rec1up, PolR.size_rec1) //. - { move=> {X0 x0 n Hsubset Hex} X0 x0 n Hx0. unfold T_power_int, TR.T_power_int. apply: Pol.dotmuldiv_correct. by rewrite size_falling_seq size_fact_seq. apply: Pol.rec1_correct =>//. + rewrite /pow_aux_rec /TR.pow_aux_rec; move=> _ _ m _. case: ifP => H. exact: J.power_int_correct. apply I.mask_correct', J.zero_correct. + exact: J.power_int_correct. } - { move=> {X0 n Hsubset Hex} Y x Hx Dx n k Hk. rewrite /T_power_int. apply: Pol.dotmuldiv_propagate; last 1 first. rewrite (@Pol.size_dotmuldiv n.+1) //. by rewrite Pol.size_rec1. by rewrite size_falling_seq. by rewrite size_fact_seq. by rewrite Pol.size_rec1 size_falling_seq. by rewrite Pol.size_rec1 size_fact_seq. apply: Pol.rec1_propagate. move=> y m _. rewrite /pow_aux_rec ifT. apply/contains_Xnan. have->: Xnan = Xpower_int^~ (p - Z.of_nat m)%Z (Xreal x). move: Dx; rewrite /Xpower_int /Xpower_int' /Xbind. by case Ep: p =>//; case: is_zero =>//; case: m. exact: I.power_int_correct. match goal with |- is_true ?a => rewrite -(negbK a) negb_or end. apply/negP; case/andP => /negbTE H0 /negbTE Hm. move: Dx; rewrite /Xpower_int. by case: {Hyp} p H0 Hm. apply/contains_Xnan. rewrite -Dx. exact: I.power_int_correct Hx. } - move=> k x Hx. have [Hp|/(apart0_correct Hx) Nx] := Hyp. apply: (ex_derive_n_ext_loc _ _ _ _ (@toR_power_int_loc p x _)). by left. by apply: ex_derive_n_powerRZ; left. apply: (ex_derive_n_ext_loc _ _ _ _ (@toR_power_int_loc p x _)). by right. by apply: ex_derive_n_powerRZ; right. 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