proposition: Lemma TM_ln_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_ln X0 X n) Xln'.
proof: Proof. move=> Hsubset Hex. rewrite /TM_ln. case E0: gt0. apply i_validTM_Ztech with (TR.T_ln tt); last 2 first =>//. exact: I.ln_correct. constructor. - by move=> {n} x [|n]; rewrite /TR.T_ln // !sizes ?(@PolR.size_dotmuldiv n.+1, PolR.size_rec1, size_rec1up, size_behead). - { move=> {X0 n Hsubset Hex} x n k Hx Hkn. rewrite (Derive_n_ext_loc _ ln); last first. apply: (locally_open (fun t => 0 < t)%R); [exact: open_gt| |exact: gt0_correct E0]. by move=> y Hy; rewrite /Xln' is_positive_true. rewrite /PolR.nth; case: k Hkn => [|k] Hkn; first by rewrite Rdiv_1. case: n Hkn => [|n] Hkn //. rewrite [nth _ _ _]PolR.nth_dotmuldiv ifF; last first. rewrite PolR.size_rec1. rewrite size_falling_seq size_behead size_fact_seq. by rewrite !orbb ltnNge -ltnS Hkn. move/(gt0_correct Hx) in E0. case: k Hkn => [|k] Hkn. simpl Derive_n; simpl INR; rewrite Rdiv_1. rewrite falling_seq_correct // nth_behead fact_seq_correct //. rewrite big_mkord big_ord0. rewrite [PolR.nth _ _]nth_rec1up /= Rdiv_1 Rmult_1_l. by rewrite (is_derive_unique _ _ _ (is_derive_ln _ E0)) Rmult_1_r. symmetry; apply: (Rmult_eq_reg_r (INR (fact k.+2))); last exact: INR_fact_neq_0. rewrite {1}/Rdiv Rmult_assoc Rinv_l ?Rmult_1_r; last exact: INR_fact_neq_0. rewrite (is_derive_n_unique _ _ _ _ (is_derive_n_ln _ _ _)) //. rewrite falling_seq_correct // nth_behead fact_seq_correct //. have Hpow: (PolR.nth (PolR.rec1 (TR.pow_aux_rec tt (-1) x) (powerRZ x (-1)) n)%R k.+1 = / x ^ (1 + k.+1))%R. rewrite /PolR.nth /PolR.rec1 nth_rec1up. rewrite ifF; last first. by apply: negbTE; rewrite ltnNge -ltnS Hkn. rewrite iteriS /TR.pow_aux_rec. suff->: powerRZ x (-1 - Z.of_nat (k + 1))%Z = / (x ^ (1 + k.+1))%R by done. rewrite pow_powerRZ -powerRZ_opp; last exact: Rgt_not_eq. congr powerRZ; change (-1)%Z with (- Z.of_nat 1)%Z. rewrite -Z.add_opp_r -Z.opp_sub_distr -Z.add_opp_r Z.opp_involutive. by f_equal; rewrite -Nat2Z.inj_add; f_equal; rewrite plusE addn1. rewrite Hpow big_mkord. rewrite -INR_IZR_INZ /Rdiv Rmult_assoc. rewrite (big_morph IZR (id1 := 1%R) (op1 := Rmult)) //; last exact: mult_IZR. set bigRhs := \big[Rmult/1%R]_i IZR _. set fk2 := INR (fact k.+2). have->: (bigRhs * / fk2 * (/ x ^ (1 + k.+1) * fk2) = (/ fk2 * fk2) * bigRhs * / (x ^ (1 + k.+1)))%R by ring. rewrite Rinv_l ?Rmult_1_l; last exact: INR_fact_neq_0. congr Rmult; rewrite {}/bigRhs. apply: eq_bigr => [[i Hi] _]. rewrite INR_IZR_INZ. rewrite Nat2Z.inj_add -opp_IZR; congr IZR. simpl Z.of_nat. by rewrite Z.opp_add_distr. } constructor. - by move=> {n X Hsubset E0} X x [|n]; rewrite /TR.T_ln !sizes //= ?(@Pol.size_dotmuldiv n.+1, Pol.size_rec1, @PolR.size_dotmuldiv n.+1, PolR.size_rec1, size_rec1up, size_behead). - { move=> {X0 x0 n Hsubset Hex} X0 x0 n Hx0. rewrite /T_ln /TR.T_ln. apply: Pol.polyCons_correct; last exact: J.ln_correct. case: n => [|n]; first exact: Pol.polyNil_correct. apply: Pol.dotmuldiv_correct; first by rewrite size_falling_seq size_behead size_fact_seq. apply: Pol.rec1_correct; first move=> *; repeat first [apply: J.div_correct |apply: J.power_int_correct |apply: J.ln_correct ]; exact: I.mask_correct'. } - { move=> {X0 n Hsubset Hex} Y x Hx Dx n k Hk. apply: Pol.polyCons_propagate. - apply/contains_Xnan. rewrite -Dx. exact: I.ln_correct Hx. - case: n Hk => [|n] Hk m; first by rewrite Pol.size_polyNil. rewrite ?(@Pol.size_dotmuldiv n.+1, Pol.size_rec1, size_falling_seq, size_behead, size_fact_seq) //. move=> Hm. apply: Pol.dotmuldiv_propagate; rewrite ?(size_falling_seq, size_behead, size_fact_seq) ?Pol.size_rec1 //. apply: Pol.rec1_propagate. move=> q l Hq. apply J.power_int_propagate, I.mask_propagate_r, contains_Xnan. by rewrite -Dx; apply: I.ln_correct Hx. apply J.power_int_propagate, I.mask_propagate_r, contains_Xnan. by rewrite -Dx; apply: I.ln_correct Hx. by rewrite ?(@Pol.size_dotmuldiv n.+1, Pol.size_rec1, size_falling_seq, size_behead, size_fact_seq). - rewrite Pol.size_polyCons. case: n Hk => [|n] Hk; first by rewrite ltnS Pol.size_polyNil. by rewrite ?(@Pol.size_dotmuldiv n.+1, Pol.size_rec1, size_falling_seq, size_behead, size_fact_seq). } - { clear - E0. move=> n x Hx. move/(gt0_correct Hx) in E0. apply: (ex_derive_n_ext_loc ln). apply: locally_open E0; first exact: open_gt. by simpl=> t Ht; rewrite /Xln' is_positive_true. exact: ex_derive_n_is_derive_n (is_derive_n_ln n x E0). } split =>//. by move=> *; rewrite I.nai_correct. by move=> Hx; rewrite /= I.nai_correct. by rewrite I.nai_correct. exact: Hsubset. exists (TR.T_ln tt x0 n). apply: Pol.polyCons_correct; case: n =>[|n]/=; first exact: Pol.polyNil_correct. - apply: Pol.dotmuldiv_correct; first by rewrite size_falling_seq size_behead size_fact_seq. apply: Pol.rec1_correct; first move=> *; repeat first [apply: J.div_correct |apply: J.power_int_correct |apply: J.ln_correct ]; exact: I.mask_correct'. - exact: J.ln_correct. - exact: J.ln_correct. by rewrite I.nai_correct. 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